on dc0332f help sign in
Idris-dev/src/Idris
1 folder, 42 files
../ Core/Tweak mergeNotunified ASTUtils.hsAdd comments. AbsSyntax.hsSimplify unused arg search. AbsSyntaxTree.hsAdd 'unify' tactic Apropos.hsMake :apropos case-insensitive CaseSplit.hsNormalise before case split Chaser.hsParser warnings; especially for invalid doc comments Colours.hsSupport text formatting in docstrings Completion.hsAdd 'unify' tactic 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 :refine (:ref) command for refining a hole Delaborate.hsMerge branch 'master' of github.com:edwinb/Idris-dev into default-arg-subst Docs.hsOnly show documented arguments in :doc Docstrings.hsEnable word-wrapping in docstrings ElabDecls.hsBetter error for ambiguous instance name ElabTerm.hsMerge 'not unified' variables Erasure.hsAdd erasure postulates for unsafePerformPrimIO. ErrReverse.hsFix for matchProblems Error.hsProvide IDESlave output with docs and type Help.hsMerge branch 'idrisdoc' of github.com:PhilipRasmussen/Idris-dev into PhilipRasmussen-idrisdoc IBC.hsAdd 'unify' tactic IdeSlave.hsAdd support for :refine to IDESlave IdrisDoc.hsIdrisDoc now merges documentation more robustly using less code. Imports.hsStrictness annotations Inliner.hsAdd a Cabal library Output.hsProvide IDESlave output with docs and type ParseData.hsUse Markdown to represent docstrings ParseExpr.hsRestored "__pi_arg" to use UN instead of MN again (due to a test failure). Removed commented out code. ParseHelpers.hsAllow argument comments to span lines ParseOps.hsRestored "__pi_arg" to use UN instead of MN again (due to a test failure). Removed commented out code. Parser.hsSimplified some lookaheads and grammar rules for lambda expressions and other internal expressions. PartialEval.hsFirst attempt now at substitution to default args Primitives.hsAdd ManagedPtr type ProofSearch.hsAdd :refine (:ref) command for refining a hole Prover.hsTweak mergeNotunified Providers.hsFirst attempt now at substitution to default args REPL.hsRemove whitespace for :addproof - like :load does REPLParser.hsMerge branch 'idrisdoc' of github.com:PhilipRasmussen/Idris-dev into PhilipRasmussen-idrisdoc 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