package coq-idt
Inductive Definition Transformers
Install
Dune Dependency
Authors
Maintainers
Sources
v1.1.0.tar.gz
sha256=054854f1e774683d0b8d14f076718eadf39a2d221f525d8a7065d12bd33948c8
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 (2)
-
coq-metacoq-template
>= "1.1" & < "1.2" -
coq
>= "8.14" & < "8.17"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page