package coq-autosubst
Coq library for parallel de Bruijn substitutions
Install
Dune Dependency
Authors
Maintainers
Sources
v1.7.tar.gz
sha512=6c118962618a0e770344e62f976826e742a16fc9206d1ea1d075c4579ad9db36985d13896787880d5dddc50cb387430328cd92c9974ccc53f8725cce46e515d5
Description
Autosubst is a library for the Coq proof assistant which provides automation for formalizing syntactic theories with variable binders. Given an inductive definition of syntactic objects in de Bruijn representation augmented with binding annotations, Autosubst synthesizes the parallel substitution operation and automatically proves the basic lemmas about substitutions.
Tags
category:Computer Science/Lambda Calculi keyword:abstract syntax keyword:binders keyword:de Bruijn indices keyword:substitution logpath:AutosubstPublished: 19 Dec 2020
Dependencies
None
Dev Dependencies (1)
-
coq
(>= "8.10" & < "8.16~") | (= "dev")
Used by
None
Conflicts
None
On This Page