git.iko.soy/Idris-dev
on 5fbca2a help sign in
history ofsrc/Idris/AbsSyntax.hs
all commits
5fbca2aFix with so that clauses are checked for matches against top level defnEdwin Brady 39b934cSugar for dependent pairsEdwin Brady 5e92c70When collecting implicit args in wheres, ignore names bound in above scopeEdwin Brady bf368abFirst attempt at with ruleEdwin Brady cc4eb28let bindings; fixed bug with simple lambda appEdwin Brady 5f7eed8Propagate line numbers through applications and variablesEdwin Brady ec87a69Some effort at reporting line numbers of errors (top level of decl only)Edwin Brady 070b0faSome unification/evaluation bug fixesEdwin Brady 180e979Added builtins.idr and fixed a bug or twoEdwin Brady b0248eaChecking syntax declarations; also allow symbolsEdwin Brady 2402885Generic syntax declarations (see prelude.idr for example)Edwin Brady 12bd089Added lifting of unsolved metavariables to global functionsEdwin Brady a7d08efdo notation (just IO at the moment - not yet overloadable)Edwin Brady 20861ecEnough Epic to compile 'hello world' (but not much else yet...)Edwin Brady 9d1ecc8Added some syntactic sugar for _|_, () and pairsEdwin Brady ca6a5e1import statementEdwin Brady 083fc70Added 'where' clauses in pattern matchesEdwin Brady de89a04Add ElabInfo to pass through elaboratorEdwin 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 59c1eb1Pretty printing of TT terms as PTermsEdwin Brady 9fe3473Added using blocksEdwin Brady 019fabaFixed unification; added well-typed interpreterEdwin Brady 739e0b5Some error handlingEdwin Brady 22b4dc4Lots of improvements in elaborating and evaluatingEdwin Brady c637850Pattern matcher, evaluation of 2+2 now worksEdwin Brady 54c8a04Checking pattern match clausesEdwin Brady 7a30f10Maybe if I add liftCatch locally things will work on 6.12Edwin Brady 174e696Don't crash on error, keep goingEdwin Brady 06a81c9Elaborating types and data declarationsEdwin Brady 8e8d57aCollect all pattern clauses for a functionEdwin Brady 1b6709fPretty printing data declarationsEdwin Brady 2050102Pretty printer for PTermEdwin Brady f85d1f0:ttshellEdwin Brady a8768afParser now fills in implicit argumentsEdwin Brady 596e9aaFunctor for PTerm/PDeclEdwin Brady 2eb5b52Pattern clause parserEdwin Brady 64b7cfdParsing high level data declarationsEdwin Brady 3b297bcParsing declarations, keeping track of fixitiesEdwin Brady 50d24ecStart of a REPL and main program with argument processingEdwin Brady 70ac28dChange fixity declarationsEdwin Brady 554c395Made a start on the high level languageEdwin Brady