git.iko.soy/Idris-dev
on ee3dbaa help sign in
history ofsrc/Typecheck.hs
all commits
5dadd08QED now rechecks the term, instead of just finalise. *bites fingernails*Edwin Brady ffd5e72arg tactic; unification tweakEdwin Brady 77be0d0Simple parser for data typesEdwin Brady 6a6a048No mucking about with de Bruijn indices in proof constructionEdwin Brady 9c6ea4aFixing evaluator bugsEdwin Brady d615021Purge HTT, fix evaluator and contextsEdwin Brady 867f092Changed evaluatorEdwin Brady bb6bba2Tactics can now complete basic proofsEdwin Brady 6923ac1Started theorem prover and tacticsEdwin Brady 205fcefSome proof state, some showing of termsEdwin Brady dc0c198First lot of source files and paperEdwin Brady