git.iko.soy/Idris-dev
on e1dc450 help sign in
Idris-dev/src/Idris
33 files
../ AbsSyntax.hsAdd ':addclause' command at the REPL AbsSyntaxTree.hsAdd :makewith command at the REPL CaseSplit.hsPick unique names for rhs when case splitting 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 ':addclause' command at the REPL ElabTerm.hsPick unique names for rhs when case splitting Error.hsAdded column name to source Help.hsTab completion for setting colours at the REPL IBC.hsAdd ':addclause' command at the REPL IdeSlave.hscleanups Imports.hsSome packaging fixes Inliner.hs%flag directive ParseData.hsFurther splitting of Parser ParseExpr.hsAdd ':addclause' command at the REPL 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.hsPick unique names for rhs when case splitting REPLParser.hsAdd :makewith command at the REPL Transforms.hsrename O into Z Unlit.hsAdded column name to source UnusedArgs.hsRemove the unused arg from lookup functions