git.iko.soy/Idris-dev
on d9a7b37 help sign in
Idris-dev/src/Idris
28 files
../ AbsSyntax.hsPartially defined names should not reduce at compile-time AbsSyntaxTree.hsAllow colour options from REPL Chaser.hsSome packaging fixes Colours.hsColourise REPL prompt Completion.hsTab completion for setting colours at the REPL Coverage.hsPartially defined names should not reduce at compile-time DSL.hsAdded 'quoteGoal x by p in e' syntax meaning, let x = p [current goal] in e Additionally, the value of x is normalised, which means p can be a compile-time only %reflection function used to prove something interesting in e. See test030 for an example of au… DataOpts.hsCompile Nat as Int, (and plus/mult/fromInteger) Delaborate.hsIndent terms printed in typechecking errors Docs.hsRemove the unused arg from lookup functions ElabDecls.hsPartially defined names should not reduce at compile-time ElabTerm.hsBetter representation and rendering of generated names Error.hsMake the type of ierror more general Help.hsTab completion for setting colours at the REPL IBC.hsCompile Nat as Int, (and plus/mult/fromInteger) IdeSlave.hscleanups Imports.hsSome packaging fixes Inliner.hs%flag directive Parser.hsPartially defined names should not reduce at compile-time 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.hsAdd skeleton of inliner 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. REPL.hsMerge pull request #480 from david-christiansen/fix-duplicate-libs REPLParser.hsAdd support for init scripts Transforms.hsrename O into Z Unlit.hsFix Unlit to cope with documentation comment syntax UnusedArgs.hsRemove the unused arg from lookup functions