SquiggleEq

Also, Sec 2.2 of the following tech report explains the core ideas behind the design of this library: http://www.nuprl.org/html/verification/verification.pdf

There is also a de-bruijn version of the above ideas. See termsDB.v

Installation:

make
sudo make install

Name		Name	Last commit message	Last commit date
Latest commit History 270 Commits
site_scons/site_tools		site_scons/site_tools
.gitignore		.gitignore
Anand_ICMS.pdf		Anand_ICMS.pdf
AssociationList.v		AssociationList.v
ExtLibMisc.v		ExtLibMisc.v
LICENCE		LICENCE
LibTactics.v		LibTactics.v
Makefile		Makefile
README.md		README.md
SConstruct		SConstruct
UsefulTypes.v		UsefulTypes.v
_CoqProject		_CoqProject
alphaeq.v		alphaeq.v
bin_rels.v		bin_rels.v
coqidescript.sh		coqidescript.sh
eq_rel.v		eq_rel.v
export.v		export.v
list.v		list.v
substitution.v		substitution.v
tactics.v		tactics.v
terms.v		terms.v
terms2.v		terms2.v
termsDB.v		termsDB.v
universe.v		universe.v
varImplDummyPair.v		varImplDummyPair.v
varImplN.v		varImplN.v
varImplPeano.v		varImplPeano.v
varImplZ.v		varImplZ.v
varInterface.v		varInterface.v
wftermSet.v		wftermSet.v

Provide feedback