git.iko.soy/Idris-dev
on 9be5866 help sign in
Idris-dev/src/Idris
1 folder, 43 files
../ Core/Make executor emulate putchar ASTUtils.hsAdd comments. AbsSyntax.hsAdapt expandParamsD to new parameter docs field in PClass AbsSyntaxTree.hsstarted working on new cmd arg parser Apropos.hsMake :apropos case-insensitive CaseSplit.hsFix interactive editing and tests Chaser.hsBring module loading into Idris monad CmdOptions.hsstarted working on new cmd arg parser 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.hsGive the pretty-printer access to info about infixes Docs.hsGive the pretty-printer access to info about infixes Docstrings.hsEnable word-wrapping in docstrings ElabDecls.hsMerge pull request #1160 from ahmadsalim/bug/furthereliminatorfixes 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.hsAdd support for :refine to IDESlave IdrisDoc.hsGive the pretty-printer access to info about infixes Imports.hsBring module loading into Idris monad Inliner.hsAdd a Cabal library Output.hsMake ihWarn work properly with emptyFC on command line ParseData.hsBug fixing of induction bugs ParseExpr.hsAdded nested record access syntax 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.hsPrevent double-printing some FCs PartialEval.hsFirst attempt now at substitution to default args Primitives.hsAdd ManagedPtr type ProofSearch.hsAdd :refine (:ref) command for refining a hole Prover.hsGive the pretty-printer access to info about infixes Providers.hsFirst attempt now at substitution to default args REPL.hsstarted working on new cmd arg parser REPLParser.hsAllow the big startup banner to be disabled 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