package coq-idt
Inductive Definition Transformers
Install
Dune Dependency
Authors
Maintainers
Sources
v1.0.1.tar.gz
sha256=d20305953c31842e33aaea318f8f84c4ad7314cb0e525d6663240abcad21099b
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.0~beta2+8.12" & < "1.1" -
coq
>= "8.12" & < "8.14~"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page