git.iko.soy/Idris-dev
on 8c19e30 help sign in
Idris-dev/src/Idris
33 files
../ AbsSyntax.hsRecord internal name of 'with' functions AbsSyntaxTree.hsRecord internal name of 'with' functions CaseSplit.hsFirst implementation of :cs (case split) REPL command 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.hsRecord internal name of 'with' functions ElabTerm.hsAdd a final unification step Error.hsAdded column name to source Help.hsTab completion for setting colours at the REPL IBC.hsRecord internal name of 'with' functions 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 error object for failure to load file 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.hsAdd CaseSplit.hs and Command (not yet implemented) REPLParser.hsAdd CaseSplit.hs and Command (not yet implemented) Transforms.hsrename O into Z Unlit.hsAdded column name to source UnusedArgs.hsRemove the unused arg from lookup functions