on ef45cdc 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.hsMerge pull request #1222 from klrr/split-bins Apropos.hs:apropos syntax for binders CaseSplit.hs:addclause now adds template bodies to instances Chaser.hsBring module loading into Idris monad CmdOptions.hsstarted working on new cmd arg parser 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.hs'search' now fails if there are metavariables Delaborate.hsAdd ppOptionIst function. Docs.hsMerge current master into fix/911- branch Docstrings.hsEnable word-wrapping in docstrings ElabDecls.hsChange type class top level method generation ElabTerm.hs'search' now fails if there are metavariables 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.hs'search' now fails if there are metavariables IdeSlave.hsAdd IDESlave support to :makelemma IdrisDoc.hsMerge branch 'master' of github.com:idris-lang/Idris-dev Imports.hsBring module loading into Idris monad Inliner.hsAdd a Cabal library Interactive.hsAdd IDESlave support to :makelemma Output.hsMake totality a warning until compiling ParseData.hsBug fixing of induction bugs ParseExpr.hs'search' now fails if there are metavariables 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.hsImplement reductions for for Buffer primitives. ProofSearch.hsFix silly error in 'search' Prover.hsShow let bindings with proper line breaks and indentation in prover Providers.hsFirst attempt now at substitution to default args REPL.hsMerge pull request #1222 from klrr/split-bins 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