Zobrazeno 1 - 1
of 1
pro vyhledávání: '"Adjedj, Arthur"'
We present an extensive mechanization of the meta-theory of Martin-L\"of Type Theory (MLTT) in the Coq proof assistant. Our development builds on pre-existing work in Agda to show not only the decidability of conversion, but also the decidability of
Externí odkaz:
http://arxiv.org/abs/2310.06376
