package coq-trocq-hott-examples
A modular parametricity plugin for proof transfer in Coq: examples
Install
Dune Dependency
Authors
Maintainers
Sources
0.2.0.tar.gz
md5=14ee380ce5141d67f34bade89c0dc8df
sha512=1827f6478eb004e358b33785bf2007ec314b46fc75324e2b2a722d9ca19a6b005d019eb5e4ab016d7b85e4f11b69e29375ef9826ab5d160fbe7ef60cad138824
Description
Tests for applications of Trocq
Tags
category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword:automation keyword:elpi keyword:proof transfer keyword:isomorphism keyword:univalence keyword:parametricity logpath:TrocqPublished: 01 Jul 2025
Dependencies (3)
- coq-mathcomp-ssreflect
- coq-trocq-hott
-
coq
>= "8.20" & < "9.1"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page