on 71bdbbb help sign in
Idris-dev/src/Idris
1 folder, 42 files
../ Core/Rule out more cases in 'recoverable' ASTUtils.hsAdd comments. AbsSyntax.hsSimplify unused arg search. AbsSyntaxTree.hsMerge branch 'repl' 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.hsAdd :refine (:ref) command for refining a hole Delaborate.hsMerge branch 'master' of github.com:edwinb/Idris-dev into default-arg-subst Docs.hsProperly pretty-print typeclasses for REPL command ':doc' Docstrings.hsEnable word-wrapping in docstrings ElabDecls.hsBetter error for ambiguous instance name 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.hs:compile now can take a codegen option (e.g. :compile javascript program.js) IBC.hsAdd 'unify' tactic IdeSlave.hsAdd support for :refine to IDESlave IdrisDoc.hsProperly pretty-print typeclasses for REPL command ':doc' 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 'repl' 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