on 90bad48 help sign in
Idris-dev/src/Idris
1 folder, 42 files
../ Core/Merge 'not unified' variables 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.hsFixed merge bug Imports.hsStrictness annotations Inliner.hsAdd a Cabal library Output.hsProvide IDESlave output with docs and type ParseData.hsUse Markdown to represent docstrings ParseExpr.hsAdd 'unify' tactic ParseHelpers.hsAllow argument comments to span lines ParseOps.hsFix parsing of $ 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.hsAdd check after each proof step, not just the end Providers.hsFirst attempt now at substitution to default args REPL.hsMerge branch 'master' of github.com:idris-lang/Idris-dev 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