Tennenbaum's Theorem in Constructive Type Theory

Compilation:

For the installation of Coq, more infos can be found here.
Tested with Coq version 8.12.2 and Equations package version 1.2.3+8.12
Using opam, these can be installed with opam install coq.8.12.2 and opam install coq-equations.1.2.3+8.12
To compile the project, run make in the project folder containing the make-file.

Name		Name	Last commit message	Last commit date
Latest commit History 41 Commits
.gitignore		.gitignore
CantorPairing.v		CantorPairing.v
Church.v		Church.v
Coding.v		Coding.v
Dec.v		Dec.v
DecidabilityFacts.v		DecidabilityFacts.v
Deduction.v		Deduction.v
Enumerability.v		Enumerability.v
FOL.v		FOL.v
Formulas.v		Formulas.v
ListEnumerabilityFacts.v		ListEnumerabilityFacts.v
Makefile		Makefile
Makefile.coq		Makefile.coq
Makefile.coq.conf		Makefile.coq.conf
Makholm.v		Makholm.v
McCarty.v		McCarty.v
NumberTheory.v		NumberTheory.v
Peano.v		Peano.v
README.md		README.md
Synthetic.v		Synthetic.v
Tarski.v		Tarski.v
Tennenbaum_diagonal.v		Tennenbaum_diagonal.v
Tennenbaum_insep.v		Tennenbaum_insep.v
Variants.v		Variants.v
WCT_Variants.v		WCT_Variants.v
_CoqProject		_CoqProject