coq-historical-examples

Historical examples developed in the (pure) Calculus of Constructions . This is a collection of historical examples developed in system CoC that implemented Coquand's Calculus of Constructions. Newman.v and Tarski.v originate in version 1.10, Manna.v and Format.v are from version 4.3. Their evolution to the Calculus of Inductive Constructions (up to Coq V6.3) are in MannaCIC.v and FormatCIC.v. (Collection by Hugo Herbelin.)

opam install coq-historical-examples.8.5.0
homepage
https://github.com/coq-contribs/historical-examples
license
LGPL 2
bugs tracker
https://github.com/coq-contribs/historical-examples/issues
dependencies
coq (>= 8.5 & < 8.6~)
source
https://github.com/coq-contribs/historical-examples/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-historical-examples/coq-historical-examples.8.5.0