package coq-autosubst

  1. Overview
  2. No Docs
Coq library for parallel de Bruijn substitutions

Install

Dune Dependency

github.com Edit opam file Versions (3)

Authors

  1. S
    Steven Schäfer
  2. T
    Tobias Tebbi

Maintainers

  1. P
    palmskog@gmail.com

Sources

v1.9.tar.gz
sha512=b78504da0cfae1e3368bc31d2cfcc63a5976b0dca2a47ce7887378cdcc6e08cba1325fac875c35562a680046f384d0379dd395422b5625bf511fa8ceb0911652

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:Autosubst date:2024-07-12

Published: 13 Jul 2024

Dependencies (1)

  1. coq >= "8.14" & < "8.21~"

Dev Dependencies

None

Used by

None

Conflicts

None