git.iko.soy/Idris-dev
on be2d7fa help sign in
history ofsrc/Core/ProofState.hs
all commits
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