git.iko.soy/Idris-dev
on ae3ad10 help sign in
Idris-dev/src/Idris
11 files
../ AbsSyntax.hsinsertImpl shouldn't crash if given too many arguments Compiler.hsAdd %include directive Delaborate.hsNo holes allowed ElabDecls.hsAdd let x = t tactic Error.hs:r and :e at the REPL. Imports.hsAdded log/exp (and lib/link directives) Parser.hsApply fromInteger for negative numbers Primitives.hsAdded Integer (but an Epic bug prevents them compiling properly) Prover.hsAdd mechanism for simplification and function options REPL.hs:t for names as well as terms REPLParser.hsAdd mechanism for simplification and function options