git.iko.soy/Idris-dev
on d8544e8 help sign in
Idris-dev/src/Idris
32 files
../ AbsSyntax.hsSome Eff experimentation, adding a 'test' command AbsSyntaxTree.hsSome Eff experimentation, adding a 'test' command Chaser.hsRefactoring of parser to Trifecta, documenting and updating some items/fixing some issues. Colours.hsAdd ability to set ANSI italics Completion.hsAdd ability to set ANSI italics Coverage.hsRemove irrelevant comment DSL.hsSome Eff experimentation, adding a 'test' command DataOpts.hsCompile Nat as Int, (and plus/mult/fromInteger) Delaborate.hsUpdate issue tracker URL Docs.hsRemove the unused arg from lookup functions ElabDecls.hsPropagate '%assert_total' to with blocks ElabTerm.hsMake more type classes resolve, by matching rather than unification Error.hsMake the type of ierror more general Help.hsTab completion for setting colours at the REPL IBC.hsCompile Nat as Int, (and plus/mult/fromInteger) IdeSlave.hscleanups Imports.hsSome packaging fixes Inliner.hs%flag directive ParseData.hsFurther splitting of Parser ParseExpr.hsChanged the way addproof works to indented-block style Allowed a larger range of expression to work with slices (improves on idris-lang/Idris-dev#524) ParseHelpers.hsFix a typo in an error message. ParseOps.hsFurther splitting of Parser Parser.hsPropagate '%assert_total' to with blocks PartialEval.hsAdd %specialise annotation for functions (Part 1 of partial evaluation) %specialise [n1 t1, n2 t2 ...] as an annotation before a function type means that the r.h.s. of all the clauses will be evaluated, but with the name n1 reduced at most t1 times, etc. T… Primitives.hsAdd '%reflection' option for functions A reflection function can evaluate at compile-time only, and pattern matches on *syntax* rather than on constructor forms. Also add 'prim__syntactic_eq' for a compile-time syntactic equality check. Prover.hsChanged the way addproof works to indented-block style Allowed a larger range of expression to work with slices (improves on idris-lang/Idris-dev#524) Providers.hsSome refactoring in CaseOp Separate case trees for totality checking, compile time and run time and lift into their own data structure, so that it's clear which one to use when. REPL.hsSplit Parser.hs into several files REPLParser.hsSplit Parser.hs into several files Transforms.hsrename O into Z Unlit.hsFix Unlit to cope with documentation comment syntax UnusedArgs.hsRemove the unused arg from lookup functions