package coq-idt
Inductive Definition Transformers
Install
Dune Dependency
Authors
Maintainers
Sources
v1.3.0.tar.gz
sha256=2a0a1c8dc7a6792e59de6b6c0c127fba09b621597bf2118c20cc57888a42a634
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.3" & < "1.4"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page