git.iko.soy/Idris-dev
on 86c9dec help sign in
Idris-dev/src/Idris
33 files
../ AbsSyntax.hsAdd --client option AbsSyntaxTree.hsAdd --client option CaseSplit.hsAdd --client option Chaser.hsConvert IO errors into erros in the Idris monad Colours.hsAdd ability to set ANSI italics Completion.hsAdd ability to set ANSI italics Coverage.hsRemove forcing optimisation from coverage checker DSL.hsAdded column name to source DataOpts.hsCompile Nat as Int, (and plus/mult/fromInteger) Delaborate.hsAdd error object for failure to load file Docs.hsRemember whether implicits are machine generated ElabDecls.hsAdd vim script to contribs/ for case split ElabTerm.hsAdd a final unification step Error.hsAdded column name to source Help.hsTab completion for setting colours at the REPL IBC.hsSupport PTerm serialisation properly IdeSlave.hscleanups Imports.hsSome packaging fixes Inliner.hs%flag directive ParseData.hsFurther splitting of Parser ParseExpr.hsMerge pull request #558 from ahmadsalim/feature/notypesaskeywords ParseHelpers.hsMerge pull request #558 from ahmadsalim/feature/notypesaskeywords ParseOps.hsChange '!' syntax and semantics to be uniform Parser.hsAdd --client option 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.hsAdded column name to source Providers.hsUse the ErrorT failure functions and attempt to preserve error structure REPL.hsMake reloading 'quiet' in --client mode REPLParser.hsAdd --client option Transforms.hsrename O into Z Unlit.hsAdded column name to source UnusedArgs.hsRemove the unused arg from lookup functions