git.iko.soy/Idris-dev
on ee3dbaa help sign in
ee3dbaaChange tactic names: fill for unify_fill and exact for fillEdwin Brady 5dadd08QED now rechecks the term, instead of just finalise. *bites fingernails*Edwin Brady 44d62c7Better if unification substitutes rather than let bindsEdwin Brady 89ffe9bUndo tacticEdwin Brady ffd5e72arg tactic; unification tweakEdwin Brady 07f3b19Add patvar tactic; fix apply to deal with names properlyEdwin Brady 12f9368apply and prepare_apply elaborationsEdwin Brady 546e9f5A gadget or twoEdwin Brady 5ee3376make Elab a state monad for ease of EDSL programmingEdwin Brady cc0dc09Added elaborate; a language for composing primitive tactics.Edwin Brady cbc60ebUnification, and unify tacticEdwin Brady 77be0d0Simple parser for data typesEdwin Brady 6a6a048No mucking about with de Bruijn indices in proof constructionEdwin Brady 1921eacSome tidying; compute; printEdwin Brady 9c6ea4aFixing evaluator bugsEdwin Brady 4c68b68EvalIn and CheckIn tacticsEdwin Brady d615021Purge HTT, fix evaluator and contextsEdwin Brady 867f092Changed evaluatorEdwin Brady 56309a5Minor parser changesEdwin Brady bb6bba2Tactics can now complete basic proofsEdwin Brady 6923ac1Started theorem prover and tacticsEdwin Brady ccd64c7Beginning of proof shellEdwin Brady 205fcefSome proof state, some showing of termsEdwin Brady f35b3f0Fix LICENSEEdwin Brady dc0c198First lot of source files and paperEdwin Brady 6aac1a9First commitEdwin Brady