NyuB / Coq-LogicalFoundation Public

Coq learning with Logical Foundation exercises

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 26 Commits
.gitignore		.gitignore
AltAuto.v		AltAuto.v
AltAutoTest.v		AltAutoTest.v
Auto.v		Auto.v
AutoTest.v		AutoTest.v
Basics.v		Basics.v
BasicsTest.v		BasicsTest.v
Bib.v		Bib.v
BibTest.v		BibTest.v
Extraction.v		Extraction.v
ExtractionTest.v		ExtractionTest.v
Imp.v		Imp.v
ImpCEvalFun.v		ImpCEvalFun.v
ImpCEvalFunTest.v		ImpCEvalFunTest.v
ImpParser.v		ImpParser.v
ImpParserTest.v		ImpParserTest.v
ImpTest.v		ImpTest.v
IndPrinciples.v		IndPrinciples.v
IndPrinciplesTest.v		IndPrinciplesTest.v
IndProp.v		IndProp.v
IndPropTest.v		IndPropTest.v
Induction.v		Induction.v
InductionTest.v		InductionTest.v
LICENSE		LICENSE
Lists.v		Lists.v
ListsTest.v		ListsTest.v
Logic.v		Logic.v
LogicTest.v		LogicTest.v
Makefile		Makefile
Makefile.coq		Makefile.coq
Makefile.coq.conf		Makefile.coq.conf
Maps.v		Maps.v
MapsTest.v		MapsTest.v
Poly.v		Poly.v
PolyTest.v		PolyTest.v
Postscript.v		Postscript.v
PostscriptTest.v		PostscriptTest.v
Preface.v		Preface.v
PrefaceTest.v		PrefaceTest.v
ProofObjects.v		ProofObjects.v
ProofObjectsTest.v		ProofObjectsTest.v
README.md		README.md
Rel.v		Rel.v
RelTest.v		RelTest.v
Tactics.v		Tactics.v
TacticsTest.v		TacticsTest.v
correct.bat		correct.bat
correct.sh		correct.sh
impdriver.ml		impdriver.ml