git.iko.soy/Idris-dev
on 175a735 help sign in
Idris-dev/src/Idris
1 folder, 44 files
../ Core/Documentation for primitives ASTUtils.hsAdd support for :set warnreach. AbsSyntax.hsMake sensible implicit choices in :addlemma AbsSyntaxTree.hsAdd :loadto command Apropos.hs:apropos syntax for binders CaseSplit.hs:addclause now adds template bodies to instances Chaser.hsBring module loading into Idris monad CmdOptions.hsFixed typo in CmdOptions to reinstate `--checkpkg` Colours.hsSupport text formatting in docstrings Completion.hsAllow the big startup banner to be disabled Coverage.hsMake totality a warning until compiling DSL.hsSyntax for failures in pattern matching let/<- DataOpts.hsRemove collapsibility and forceability altogether. DeepSeq.hsAdd :loadto command Delaborate.hsAdd ppOptionIst function. Docs.hsMerge current master into fix/911- branch Docstrings.hsEnable word-wrapping in docstrings ElabDecls.hsMake sure binders are unique before case tree ElabTerm.hsAdd an optional depth to 'search' tactic Erasure.hsRemember names of deBruijn variables. ErrReverse.hsFix for matchProblems Error.hsProvide IDESlave output with docs and type Help.hsRemove the REPL Info command IBC.hsAdd :loadto command IdeSlave.hsAdd IDESlave support to :makelemma IdrisDoc.hsAdd an optional depth to 'search' tactic Imports.hsBring module loading into Idris monad Inliner.hsAdd a Cabal library Interactive.hsAdd an optional depth to 'search' tactic Output.hsMake totality a warning until compiling ParseData.hsBug fixing of induction bugs ParseExpr.hsAdd an optional depth to 'search' tactic ParseHelpers.hsFix zero argument with clauses ParseOps.hsRestored "__pi_arg" to use UN instead of MN again (due to a test failure). Removed commented out code. Parser.hsAdd :loadto command PartialEval.hsFirst attempt now at substitution to default args Primitives.hsImplement reductions for for Buffer primitives. ProofSearch.hsAdd an optional depth to 'search' tactic Prover.hsCheck that proof steps introduce no new problems Providers.hsFirst attempt now at substitution to default args REPL.hsAdd :loadto command REPLParser.hsAdd :loadto command Transforms.hsUse Data.Text for variable names Unlit.hsPrepared data structure of FC for spanning, and added the span of the last token parsed to Idris WhoCalls.hsAdd :who-calls and :calls-who to IDESlave