package coq-idt
Inductive Definition Transformers
Install
Dune Dependency
Authors
Maintainers
Sources
v1.2.0.tar.gz
sha256=55d9552917e41769fa18f3823eef3d1910067bd33646bf4ddce2d90b2258725e
Description
This Coq library allows you to transform an inductive definition to another inductive definition, by providing a constructor transformer tactic. It can be used to generate boilerplate lemmas for backward and forward reasoning, and to generate inductive types with many similar cases.
Dependencies (1)
-
coq-metacoq-template
>= "1.2" & < "1.3"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page