git.iko.soy/Idris-dev
on cc99207 help sign in
Idris-dev/src/Idris
1 folder, 45 files
../ Core/Unify more things! ASTUtils.hsAdd support for :set warnreach. AbsSyntax.hsPostpone implicit addition in case blocks AbsSyntaxTree.hsMake load to line work with mutual blocks 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.hsFind negative occurrences in positivity checker DSL.hsSyntax for failures in pattern matching let/<- DataOpts.hsRemove collapsibility and forceability altogether. DeepSeq.hsMake load to line work with mutual blocks Delaborate.hsAdd ppOptionIst function. Docs.hsMerge current master into fix/911- branch Docstrings.hsEnable word-wrapping in docstrings ElabDecls.hsExtend positivity check for mutual data types ElabTerm.hsUnify more things! Erasure.hsRemember names of deBruijn variables. ErrReverse.hsFix for matchProblems Error.hsFix missing function call from 723d972b2 Help.hsRemove the REPL Info command IBC.hsMake load to line work with mutual blocks IdeSlave.hsIDESlave support for :loadto IdrisDoc.hsAdd an optional depth to 'search' tactic Imports.hsBring module loading into Idris monad Inliner.hsAdd a Cabal library Interactive.hsIDESlave support for setting the depth of interactive proof search 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.hsMake load to line work with mutual blocks PartialEval.hsFirst attempt now at substitution to default args Primitives.hsEffect handlers should be covering 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.hsNow we can handle typeclasses! REPLParser.hsPreliminary version of type-directed search Transforms.hsUse Data.Text for variable names TypeSearch.hsNow we can handle typeclasses! 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