coq-autosubst.opam

# This file was generated from `meta.yml`, please do not edit manually.
# Follow the instructions on https://github.com/coq-community/templates to regenerate.

opam-version: "2.0"
maintainer: "palmskog@gmail.com"
version: "dev"

homepage: "https://github.com/coq-community/autosubst"
dev-repo: "git+https://github.com/coq-community/autosubst.git"
bug-reports: "https://github.com/coq-community/autosubst/issues"
license: "MIT"

synopsis: "Coq library for parallel de Bruijn substitutions"
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."""

build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
  "coq" {(>= "8.14" & < "8.21~") | (= "dev")}
]

tags: [
  "category:Computer Science/Lambda Calculi"
  "keyword:abstract syntax"
  "keyword:binders"
  "keyword:de Bruijn indices"
  "keyword:substitution"
  "logpath:Autosubst"
]
authors: [
  "Steven Schäfer"
  "Tobias Tebbi"
]