git.iko.soy/Idris-dev
on be2d7fa help sign in
history ofsrc/Core/TT.hs
all commits
4931c20Added Integer (but an Epic bug prevents them compiling properly)Edwin Brady 814ebdaMake sure patterns are in dependency orderEdwin Brady 188dda5Tinkering with tactics and deferred definitionsEdwin Brady 7b1336bFixed naming problem in type checking of applicationEdwin Brady 3bdfa26Added [static] annotations (which do nothing yet) and state to evaluatorEdwin Brady 6757c47Added case analysis on types, but only when enabled with --typecase (since it breaks parametricity)Edwin Brady 5fbca2aFix with so that clauses are checked for matches against top level defnEdwin Brady 5e92c70When collecting implicit args in wheres, ignore names bound in above scopeEdwin Brady bf368abFirst attempt at with ruleEdwin Brady ec87a69Some effort at reporting line numbers of errors (top level of decl only)Edwin Brady 070b0faSome unification/evaluation bug fixesEdwin Brady 12bd089Added lifting of unsolved metavariables to global functionsEdwin Brady 868409aSmall bug fixesEdwin Brady 083fc70Added 'where' clauses in pattern matchesEdwin Brady a2a5141Allow interleaving of explicit and implicit arguments in top level typesEdwin Brady a805f47Added constants and some primitive operationsEdwin Brady f9fb363Tinkering with error reportingEdwin Brady 019fabaFixed unification; added well-typed interpreterEdwin Brady 22b4dc4Lots of improvements in elaborating and evaluatingEdwin Brady c637850Pattern matcher, evaluation of 2+2 now worksEdwin Brady 17e22afFeed a type to the elaborator for the RHS of a pattern. Also, change type of pattern bindersEdwin Brady 1b6709fPretty printing data declarationsEdwin Brady a8768afParser now fills in implicit argumentsEdwin Brady 82585e7Some ghc 6.12 compatibilityEdwin Brady 554c395Made a start on the high level languageEdwin Brady ff5f762Rename Core to TTEdwin Brady