on 46256ab help sign in
Idris-dev/src/Idris
33 files
../ AbsSyntax.hsAdd ':addclause' command at the REPL AbsSyntaxTree.hsAdd ':addclause' command at the REPL CaseSplit.hsAdd ':addclause' command at the REPL 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.hsAdd a final unification step 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.hsAdd ':addclause' command at the REPL REPLParser.hsAdd ':addclause' command at the REPL Transforms.hsrename O into Z Unlit.hsAdded column name to source UnusedArgs.hsRemove the unused arg from lookup functions