package coq-autosubst-ocaml
OCaml implementation of Autosubst 2 for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
1.1+8.19.tar.gz
sha256=b197053a8201e5de41668dfa4a91c8be00f901508b66f969aeae78d382d66633
Description
Autosubst 2 can be used to generate substitution boilerplate code for syntax with binders. It takes language definitions written in signature files and outputs a file that contains Coq code implementing the language, the substitution operation, rewriting lemmas and a tactic to automatically solve certain substitution goals using the rewriting lemmas.
Published: 06 Feb 2024
Dependencies (6)
-
ppx_deriving
>= "5.2.1" -
ocamlgraph
>= "2.0.0" -
dune
>= "2.5" -
angstrom
>= "0.15.0" -
coq
>= "8.19" & < "8.20" -
ocaml
>= "4.09" & < "4.15"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page