git.iko.soy/Idris-dev
on 496cf41 help sign in
history ofsrc/Core/ProofState.hs
all commits
dd5001fmake TT aware of Set -> Typeraichoo 4a9c0f4Fix argument names in generated types for where blocksEdwin Brady c10146bLimited type inference of types in where clauses Type signatures can now be omitted *only* if the type of the function can be determined completely from the first call.Edwin Brady f833918(Experimental) Create deferred definitions by applicationEdwin Brady 1677c30Better dealing with name shadowing while building instances ...and while type checking completed termsEdwin Brady 56223efDon't normalise everywhere!Edwin Brady ca684b6Fix pToV scoping bugEdwin Brady f9a1dabFix pattern variable problem when patterns generated by unificationEdwin Brady 28ecd81Erase unused arguments when compilingEdwin 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 611dd97Improve speed of type checking by spotting unification failure quickerEdwin Brady 6cb70bcFix for simple function applicationsEdwin Brady 96031d1Normalise rewrite rule so that they apply more easilyEdwin Brady 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 4bcfa68Tinker with specialisationEdwin Brady 33baa44More on errors; propagate line numbersEdwin Brady 6682ebbPropagate solutions properlyEdwin Brady 558d226Update elaborator for application of local variablesEdwin Brady 33bf2bdUnification tweakEdwin Brady d1d672eCollect all unification errors instead of immediately reporting failureEdwin Brady 02881b1Implemented forcing optimisation Constructor arguments which are inferrable from the indices in the constructor type are erased both at compile-time and run-timeEdwin Brady 1823cf9Postpone injectivity check until after unificationEdwin Brady 7384683Fiddle with elaborator; update interp sample and testEdwin Brady b26716aCollect cumulativity constraints on universesEdwin Brady 03d7d5eAllow type labels on lambdasEdwin Brady bbaa193Better representation of namesEdwin Brady 229a99cBetter elaboration order; also changed instance argument syntax slightlyEdwin Brady ed64e76Better type class resolutionsEdwin Brady be3a53aType class instance resolution, and some Num overloadingEdwin Brady 1b1a055Improved where; implicit arguments now expanded during elaborationEdwin Brady 188dda5Tinkering with tactics and deferred definitionsEdwin Brady 7b1336bFixed naming problem in type checking of applicationEdwin Brady 58bd7c4Added rewrite tacticEdwin Brady 551548cBeginning theorem prover interfaceEdwin Brady b85965eparser tinkeringEdwin Brady cc4eb28let bindings; fixed bug with simple lambda appEdwin Brady 12bd089Added lifting of unsolved metavariables to global functionsEdwin Brady f9fb363Tinkering with error reportingEdwin Brady 739e0b5Some error handlingEdwin Brady 22b4dc4Lots of improvements in elaborating and evaluatingEdwin Brady 17e22afFeed a type to the elaborator for the RHS of a pattern. Also, change type of pattern bindersEdwin Brady 54c8a04Checking pattern match clausesEdwin Brady 06a81c9Elaborating types and data declarationsEdwin Brady aa85339Builds on ubuntu haskell platformEdwin Brady ff5f762Rename Core to TTEdwin Brady 0ae24f1Shift core TT into a separate directory (for ease of reuse)Edwin Brady