on 5dadd08 help sign in
all commits
89ffe9bUndo tacticEdwin Brady 5ee3376make Elab a state monad for ease of EDSL programmingEdwin Brady cc0dc09Added elaborate; a language for composing primitive tactics.Edwin Brady 6a6a048No mucking about with de Bruijn indices in proof constructionEdwin Brady 1921eacSome tidying; compute; printEdwin Brady 867f092Changed evaluatorEdwin Brady bb6bba2Tactics can now complete basic proofsEdwin Brady 6923ac1Started theorem prover and tacticsEdwin Brady ccd64c7Beginning of proof shellEdwin Brady