git.iko.soy/Idris-dev
on d8fffa2 help sign in
Idris-dev/src/Idris
32 files
../ AbsSyntax.hsFix bug in scoping rules for pattern matches AbsSyntaxTree.hsSupport '!' at 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.hsChange '!' syntax and semantics to be uniform DataOpts.hsCompile Nat as Int, (and plus/mult/fromInteger) Delaborate.hsRemember whether implicits are machine generated Docs.hsRemember whether implicits are machine generated ElabDecls.hsUse the ErrorT failure functions and attempt to preserve error structure ElabTerm.hsChange '!' syntax and semantics to be uniform Error.hsUpdate compiler to use new error handling Help.hsTab completion for setting colours at the REPL IBC.hsMerge branch 'master' of github.com:edwinb/Idris-dev into implicit-bind IdeSlave.hscleanups Imports.hsSome packaging fixes Inliner.hs%flag directive ParseData.hsFurther splitting of Parser ParseExpr.hsSupport '!' at REPL ParseHelpers.hsFix a typo in an error message. ParseOps.hsChange '!' syntax and semantics to be uniform Parser.hsMerge branch 'master' of github.com:edwinb/Idris-dev into implicit-bind 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.hsConvert IO errors into erros in the Idris monad Providers.hsUse the ErrorT failure functions and attempt to preserve error structure REPL.hsCheck for file extension in :e REPLParser.hsSplit Parser.hs into several files Transforms.hsrename O into Z Unlit.hsUse the ErrorT failure functions and attempt to preserve error structure UnusedArgs.hsRemove the unused arg from lookup functions