on dda9b49 help sign in
Idris-dev/src/Idris
1 folder, 42 files
../ Core/Merge pull request #1143 from ahmadsalim/bug/inductionfix ASTUtils.hsAdd comments. AbsSyntax.hsBug fixing of induction bugs AbsSyntaxTree.hsMerge branch 'master' into fix/1047-repl-doc-for-typeclasses Apropos.hsMake :apropos case-insensitive CaseSplit.hs:makewith works with .lidr now 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.hsBug fixing of induction bugs Delaborate.hsMerge branch 'master' of github.com:edwinb/Idris-dev into default-arg-subst Docs.hsDisplay docstrings for typeclass parameters and simplify dispaly of subclasses Docstrings.hsEnable word-wrapping in docstrings ElabDecls.hsGenerate better record update functions 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.hsBug fixing of induction bugs IdeSlave.hsAdd support for :refine to IDESlave IdrisDoc.hsMerge branch 'master' into fix/1047-repl-doc-for-typeclasses Imports.hsStrictness annotations Inliner.hsAdd a Cabal library Output.hsProvide IDESlave output with docs and type ParseData.hsBug fixing of induction bugs ParseExpr.hsNested record update syntax 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.hsNested record update syntax REPLParser.hsRemove the REPL Info command 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