package coq-catt-plugin
A Coq plugin for the catt proof-assistant
Install
Dune Dependency
Authors
Maintainers
Sources
catt-1.0.tbz
sha256=20a0b4aae3655274cb7336cb158699ceb1ee29909e50405d0ccb9d54d985baeb
sha512=1919da8eea60817a0907be4aa6f399a9e66fc8746d190ea805de8721a44f5f8a68b9c67626b7767e42a7cd0f061e00c16cd6c63570cbdedf15bc31f8b598f72b
doc/CHANGES.html
1.0 (2024-10)
Coq catt plugin
- Working export of catt term into coq
Catt
- Computation of 1-naturality
- Computation of functorialisation
- Computation of inverses and cancellation witnesses
- Computation of opposites
- Builtin identities and compositions
- Computation of suspension and implicit suspension
- Inference of implicit variables
- Basic type checker
On This Page