git.iko.soy/Idris-dev
on aa7262e help sign in
history ofsrc/Idris/Prover.hs
all commits
f9a1dabFix pattern variable problem when patterns generated by unificationEdwin Brady 2fb2445indent proof blocks by 2 spacesraichoo 9affb75Totality checker improvements Now does a better job of checking type class instances for totality, by inlining dictionaries where possible. Added %default total declarations to some libraries where possibleEdwin Brady 5a6299bUnification fix Specifically to stop it filling in things which are given by the programmer (caused by a bug replacing nullary constructors with terms!)Edwin Brady 8063cfdAdded --dumpcases <file> option for dumping case trees on compilingEdwin Brady 0f957f6Add Proj operator to runtime version of TT Allows extracting arguments without checking constructor first which will make erasing unused values easier shortlyEdwin Brady b8815e2added proof listraichoo 19495edCheck patterns are inaccessibleEdwin Brady 489ea6fPass pattern variable names to match compilerEdwin Brady 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