git.iko.soy/Idris-dev
on f8e6549 help sign in
Idris-dev/src/Idris
1 folder, 43 files
../ Core/Documentation for primitives ASTUtils.hsAdd support for :set warnreach. AbsSyntax.hsImprove ideslave highlighting of primitives AbsSyntaxTree.hsAdd :makelemma command in interactive editing Apropos.hs:apropos syntax for binders CaseSplit.hs:addclause now adds template bodies to instances Chaser.hsBring module loading into Idris monad 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 a field for parameter docstrings in the PClass constructor of PDecl' Delaborate.hsAdd ppOptionIst function. Docs.hsMerge pull request #1208 from david-christiansen/primitive-docs Docstrings.hsEnable word-wrapping in docstrings ElabDecls.hs:addclause now adds template bodies to instances ElabTerm.hsAdd :makelemma command in interactive editing Erasure.hsAdd erasure postulates for unsafePerformPrimIO. ErrReverse.hsFix for matchProblems Error.hsProvide IDESlave output with docs and type Help.hsRemove the REPL Info command IBC.hsMake totality a warning until compiling IdeSlave.hsDocumentation for primitives IdrisDoc.hsImprove ideslave highlighting of primitives Imports.hsBring module loading into Idris monad Inliner.hsAdd a Cabal library Interactive.hs:addclause now adds template bodies to instances Output.hsMake totality a warning until compiling ParseData.hsBug fixing of induction bugs ParseExpr.hsFix Haddock build problems ParseHelpers.hsAdd a field for parameter docstrings in the PClass constructor of PDecl' ParseOps.hsRestored "__pi_arg" to use UN instead of MN again (due to a test failure). Removed commented out code. Parser.hsMerge pull request #1204 from david-christiansen/totality-warning PartialEval.hsFirst attempt now at substitution to default args Primitives.hsAdd primitive for stdout, stderr ProofSearch.hsAdd :refine (:ref) command for refining a hole Prover.hsShow let bindings with proper line breaks and indentation in prover Providers.hsFirst attempt now at substitution to default args REPL.hsAdd :makelemma command in interactive editing REPLParser.hsAdd :makelemma command in interactive editing 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