git.iko.soy/Idris-dev
on aabd0a9 help sign in
Idris-dev/src/Idris
1 folder, 42 files
../ Core/Improve ideslave highlighting of primitives ASTUtils.hsAdd support for :set warnreach. AbsSyntax.hsImprove ideslave highlighting of primitives AbsSyntaxTree.hsImprove ideslave highlighting of primitives Apropos.hs:apropos syntax for binders CaseSplit.hsFix interactive editing and tests Chaser.hsBring module loading into Idris monad Colours.hsSupport text formatting in docstrings Completion.hsAllow the big startup banner to be disabled Coverage.hsAllow second argument of assert_smaller to be of different type than first argument since this could be useful for functions that are written with Universe-style pattern matching, i.e., where the rhs pattern has different type than the lhs expression. 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.hsAdd ppOptionIst function. Docstrings.hsEnable word-wrapping in docstrings ElabDecls.hsChange impl argument to a pretty printing opt record ElabTerm.hsMerge pull request #1130 from jonsterling/fix/reify-intro-induction 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.hsBring module loading into Idris monad IdeSlave.hsImprove ideslave highlighting of primitives IdrisDoc.hsImprove ideslave highlighting of primitives Imports.hsBring module loading into Idris monad Inliner.hsAdd a Cabal library Output.hsMerge pull request #1183 from pminten/ppopt 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.hsAllow %name to take an infix name as an argument. PartialEval.hsFirst attempt now at substitution to default args Primitives.hsAdd ManagedPtr type 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 support for :set warnreach. REPLParser.hsAdd support for :set warnreach. 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