git.iko.soy/Idris-dev
on 1b6709f help sign in
history ofsrc/Main.hs
all commits
1b6709fPretty printing data declarationsEdwin Brady 2050102Pretty printer for PTermEdwin Brady a8768afParser now fills in implicit argumentsEdwin Brady 3b297bcParsing declarations, keeping track of fixitiesEdwin Brady 50d24ecStart of a REPL and main program with argument processingEdwin Brady 554c395Made a start on the high level languageEdwin Brady ff5f762Rename Core to TTEdwin Brady 0ae24f1Shift core TT into a separate directory (for ease of reuse)Edwin Brady ac25f15Changed contexts to Data.MapEdwin Brady 44d62c7Better if unification substitutes rather than let bindsEdwin Brady cc0dc09Added elaborate; a language for composing primitive tactics.Edwin Brady 867f092Changed evaluatorEdwin Brady 6923ac1Started theorem prover and tacticsEdwin Brady 205fcefSome proof state, some showing of termsEdwin Brady dc0c198First lot of source files and paperEdwin Brady