package coq-ptsf
Explicit Convertibility Proofs in Pure Type Systems
Install
Dune Dependency
Authors
Maintainers
Sources
v8.10.0.tar.gz
md5=f5f68932253b4db6d1168b2cb41f7e09
Description
Formalization of the proof that PTS and PTS with explicit convertibility proofs (PTSf) are equivalent.
Tags
keyword: pure type systems keyword: judgmental equality keyword: explicit equality proofs keyword: proof relevance category: Mathematics/Logic/Type theoryPublished: 07 Dec 2019
Dependencies (3)
-
coq-ptsatr
>= "8.10" & < "8.11~" -
coq
>= "8.10" & < "8.11~" - ocaml
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page