git.iko.soy/Idris-dev
on 602ce01 help sign in
history ofsrc/Idris/Prover.hs
all commits
368fdf6Some playing around with widths to make everything look nicer.Dominic Mulligan c824099Major improvement to pretty printing of proof states, especially when the goal is a large term.Dominic Mulligan 8c64e9cGot pretty printing partially working using the Pretty type class as a replacement for Show. Now need to tweak it in order to make everything look nice, and to get terms printing correctly!Dominic Mulligan ab039f2Fix universe checking bugEdwin Brady e39254cAdded 'abandon' command in proof mode (Alternatively, :q)Edwin Brady 6682ebbPropagate solutions properlyEdwin Brady a3c6231:addproof knows about .lidr filesEdwin Brady 33bf2bdUnification tweakEdwin Brady 1112fe4Coverage checker Not quite complete - a bug (which I know how to fix) makes some things appear not covering even though they are. Results currently used only for pruning case trees in compiled code. There is a small performance penalty - coverage checking can be disable with --nocoverageEdwin Brady baaba44Run-time forcing optimisationEdwin Brady 4ca34ffFix error recovery in replEdwin Brady 49e426aSwitch from readline to haskelineMathnerd314 2e9fcd4Remove semicolons in tutorialEdwin Brady 67c5734Added case and pattern matching let bindings Also pattern matching bind in do notation case notation currently has limitations: - only works on simple types (each pattern must have the same type, more specifically) - return type needs to be known at the point of elaborationEdwin Brady 1823cf9Postpone injectivity check until after unificationEdwin Brady dcc09e0Fix metavariable naming in namespacesEdwin Brady acb1f19Add :a comment, to add most recent proof script to source fileEdwin Brady 8cd093fChanged lookup to return a list (preparation for namespaces)Edwin Brady 07f12f9Separate elaboration of declarations and termsEdwin Brady b26716aCollect cumulativity constraints on universesEdwin Brady ffc64e3Add mechanism for simplification and function optionsEdwin Brady be3a53aType class instance resolution, and some Num overloadingEdwin Brady 1b1a055Improved where; implicit arguments now expanded during elaborationEdwin Brady f7a7f0bSome proofs in nat.idrEdwin Brady 58bd7c4Added rewrite tacticEdwin Brady 10b88aeAdded refine, focus, undoEdwin Brady ebcb29bAdded proof script traces for pasting into programEdwin Brady 551548cBeginning theorem prover interfaceEdwin Brady