git.iko.soy/Idris-dev
on bbaa193 help sign in
history ofsrc/Core/Elaborate.hs
all commits
bbaa193Better representation of namesEdwin Brady 1c49219Added provisional definitionsEdwin Brady e0e52f1simple_app should try both elaboration ordersEdwin Brady f31caf5unique_hole needs to check whole contextEdwin Brady 71c1a0eExtension parsing, now deferring checks name is uniqueEdwin Brady 2c05448Give invented pattern variables unique namesEdwin Brady f2368e9More care with naming in where clausesEdwin 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 188dda5Tinkering with tactics and deferred definitionsEdwin Brady 58bd7c4Added rewrite tacticEdwin Brady 10b88aeAdded refine, focus, undoEdwin Brady 551548cBeginning theorem prover interfaceEdwin Brady 7c4f79cSome progress towards specialisationEdwin Brady cc4eb28let bindings; fixed bug with simple lambda appEdwin Brady ec87a69Some effort at reporting line numbers of errors (top level of decl only)Edwin Brady 12bd089Added lifting of unsolved metavariables to global functionsEdwin Brady a2a5141Allow interleaving of explicit and implicit arguments in top level typesEdwin Brady e613365All names introduced by nachine should be MN, to avoid clashesEdwin Brady 019fabaFixed unification; added well-typed interpreterEdwin 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 50d24ecStart of a REPL and main program with argument processingEdwin Brady ff5f762Rename Core to TTEdwin Brady 0ae24f1Shift core TT into a separate directory (for ease of reuse)Edwin Brady