git.iko.soy/Idris-dev
on f35d483 help sign in
Idris-dev/src/Idris
6 folders, 47 files
../ Core/Remove old eliminator generation and induction tactic (#4351) Elab/Remove old eliminator generation and induction tactic (#4351) Info/Alphabetize and indent imports and LANGUAGE pragmas Package/[ fix #4255 ] Not silently accepting invalid options Parser/Remove old eliminator generation and induction tactic (#4351) REPL/Improve error message locations (#4210) ASTUtils.hsRemove the empty property 'copyright'. AbsSyntax.hsAllow capitalized pattern variables via switch AbsSyntaxTree.hsRemove old eliminator generation and induction tactic (#4351) Apropos.hsRemove the empty property 'copyright'. CaseSplit.hsRemove the empty property 'copyright'. Chaser.hsFix efficiency problem with module chasing CmdOptions.hsAllow capitalized pattern variables via switch Colours.hsRemove the empty property 'copyright'. Completion.hsImprove error message locations (#4210) Coverage.hsFix checking if error is recoverable wrt coverage DSL.hsAdd alternatives syntax to `let` in `do` blocks DataOpts.hsRemove the empty property 'copyright'. DeepSeq.hsRemove the empty property 'copyright'. Delaborate.hsRemove old eliminator generation and induction tactic (#4351) Directives.hsRemove the empty property 'copyright'. Docs.hsRemove the empty property 'copyright'. Docstrings.hsRemove the empty property 'copyright'. ElabDecls.hsRemove the empty property 'copyright'. Erasure.hsRemove the empty property 'copyright'. ErrReverse.hsRemove the empty property 'copyright'. Error.hsAdd alternatives syntax to `let` in `do` blocks Help.hsRemove the empty property 'copyright'. IBC.hsBump IBC version after removing `%elim` items IdeMode.hsRemove the empty property 'copyright'. IdrisDoc.hsRemove old eliminator generation and induction tactic (#4351) Imports.hsRemove the empty property 'copyright'. Info.hsRemove the empty property 'copyright'. Inliner.hsRemove the empty property 'copyright'. Interactive.hsRemove the empty property 'copyright'. Main.hsRename to emitWarning ModeCommon.hsFix efficiency problem with module chasing Options.hsAllow capitalized pattern variables via switch Output.hsRename to emitWarning Package.hsSet environment with Idris flags while running `make` Parser.hs[ fix ] handle empty NS + test case PartialEval.hsRemove the empty property 'copyright'. Primitives.hsRemove the empty property 'copyright'. ProofSearch.hsRemove the empty property 'copyright'. Prover.hsFormat some messages in the prover Providers.hsRemove the empty property 'copyright'. REPL.hsPrint error message if :exec'ed program exits with failure Reflection.hsRemove old eliminator generation and induction tactic (#4351) Termination.hsFix efficiency problem with 'covering' Transforms.hsRemove the empty property 'copyright'. TypeSearch.hsRemove the empty property 'copyright'. Unlit.hsRemove the empty property 'copyright'. WhoCalls.hsRemove the empty property 'copyright'.