package coq-subst

  1. Overview
  2. Homepage
The confluence of Hardin-Lévy lambda-sigma-lift-calcul

Install

Dune Dependency

Authors

Maintainers

Sources

v8.6.0.tar.gz
md5=ec5d84b616435ee0e09716cd6fdbdc36

Description

The confluence of Hardin-Lévy lambda-sigma-lift-calcul is proven. By the way, several standard definition and results about rewriting systems are proven (Newman's lemma, Yokouchi's lemma, ...).

Dependencies (2)

  1. coq >= "8.6" & < "8.7~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover