git.iko.soy/Idris-dev
on 180e979 help sign in
180e979Added builtins.idr and fixed a bug or twoEdwin Brady 834a5e0Fix bug in applying syntax rulesEdwin 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 7ea4422added vect.idrEdwin Brady a7d08efdo notation (just IO at the moment - not yet overloadable)Edwin Brady 1c9392etinker tinkerEdwin Brady bda1f6fMore of the compilerEdwin Brady 4436bcbAdded Idris.CompilerEdwin Brady 20861ecEnough Epic to compile 'hello world' (but not much else yet...)Edwin Brady 38a6bc7Added some library filesEdwin Brady 9d1ecc8Added some syntactic sugar for _|_, () and pairsEdwin Brady 868409aSmall bug fixesEdwin Brady bcdde4aMakefile addedEdwin Brady f208c49Library checkingEdwin Brady 20bf4d7Added lib/ and preludeEdwin Brady b1419b2Allow whitespace before program textEdwin Brady ca6a5e1import statementEdwin Brady db7f0c1Paper structure; delete useless codeEdwin Brady 3b115b2Fixed pattern matching and delaborator bugEdwin 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 7123e31Float operationsEdwin Brady a805f47Added constants and some primitive operationsEdwin Brady f9fb363Tinkering with error reportingEdwin Brady 59c1eb1Pretty printing of TT terms as PTermsEdwin Brady d3adb11Allow argument lists in lambda and pisEdwin Brady 9fe3473Added using blocksEdwin Brady e613365All names introduced by nachine should be MN, to avoid clashesEdwin Brady 2378a62Convert holes to patterns when evaluating at the prompt, for displayEdwin Brady 012b595Gratuitous interpreter extension to exercise the elaborator moreEdwin Brady f97602bmore interpreter testingEdwin 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 17e22afFeed a type to the elaborator for the RHS of a pattern. Also, change type of pattern bindersEdwin Brady 54c8a04Checking pattern match clausesEdwin Brady 7a30f10Maybe if I add liftCatch locally things will work on 6.12Edwin Brady be2b9bcAdd ElabDeclsEdwin Brady 174e696Don't crash on error, keep goingEdwin Brady 06a81c9Elaborating types and data declarationsEdwin Brady efd11bbOopsEdwin 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