../ AbsSyntax.hsRemember whether implicits are machine generated13 years ago AbsSyntaxTree.hsRemember whether implicits are machine generated13 years ago Chaser.hsRefactoring of parser to Trifecta, documenting and updating some items/fixing some issues.13 years ago Colours.hsAdd ability to set ANSI italics13 years ago Completion.hsAdd ability to set ANSI italics13 years ago Coverage.hsRemove forcing optimisation from coverage checker13 years ago DSL.hsSome Eff experimentation, adding a 'test' command13 years ago DataOpts.hsCompile Nat as Int, (and plus/mult/fromInteger)13 years ago Delaborate.hsRemember whether implicits are machine generated13 years ago Docs.hsRemember whether implicits are machine generated13 years ago ElabDecls.hsRemember whether implicits are machine generated13 years ago ElabTerm.hsRemember whether implicits are machine generated13 years ago Error.hsMake the type of ierror more general13 years ago Help.hsTab completion for setting colours at the REPL13 years ago IBC.hsRemember whether implicits are machine generated13 years ago IdeSlave.hscleanups13 years ago Imports.hsSome packaging fixes13 years ago Inliner.hs%flag directive13 years ago ParseData.hsFurther splitting of Parser13 years ago ParseExpr.hsMerge branch 'feature/simplifiedparsing' of https://github.com/ahmadsalim/Idris-dev into ahmadsalim-feature/simplifiedparsing13 years ago ParseHelpers.hsFix a typo in an error message.13 years ago ParseOps.hsFurther splitting of Parser13 years ago Parser.hsPropagate '%assert_total' to with blocks13 years ago 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…13 years ago 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.13 years ago Prover.hsChanged the way addproof works to indented-block style Allowed a larger range of expression to work with slices (improves on idris-lang/Idris-dev#524)13 years ago Providers.hsSome refactoring in CaseOp Separate case trees for totality checking, compile time and run time and lift into their own data structure, so that it's clear which one to use when.13 years ago REPL.hsFixes idris-lang/Idris-dev#51213 years ago REPLParser.hsSplit Parser.hs into several files13 years ago Transforms.hsrename O into Z13 years ago Unlit.hsFix Unlit to cope with documentation comment syntax14 years ago UnusedArgs.hsRemove the unused arg from lookup functions14 years ago