git.iko.soy/Idris-dev
on ee8fce0 help sign in
Idris-dev/src/Idris
2 folders, 46 files
../ Core/Begin implementation of reflected elab monad Elab/Expose equality proofs in with rule ASTUtils.hsTidy up the IState when classes are undefined AbsSyntax.hsPlumb source locations through Tactical's elab AbsSyntaxTree.hsMerge branch 'wip/tactical' of https://github.com/david-christiansen/Idris-dev into david-christiansen-wip/tactical Apropos.hsAdd scoped implicit argument to Pi CaseSplit.hsCreate a proper name supply for identity type Chaser.hsAllow documentation for modules CmdOptions.hsRename ideslave to ide-mode Colours.hsIndicate the end of each escape sequence in the prompt string, since there's no way for Haskeline to detect it automatically. Completion.hsAdd function to list installed packages Coverage.hsMake some comments into proper Haddock DSL.hsDesugar do blocks inside of %runTactics DataOpts.hsAdded TODO for DataOpts.hs DeepSeq.hsPlumb source locations through Tactical's elab Delaborate.hsFix the new totality test Docs.hsAllow documentation for modules Docstrings.hsRemove -Werror from all files ElabDecls.hsSupport scoped type class constraints ElabQuasiquote.hsPlumb source locations through Tactical's elab ElabTerm.hsAdd "intro" tactic to new tactics Erasure.hsErasure should ignore Type*/UniqueType ErrReverse.hs Error.hsAdd missing cases to warnDisamb Help.hsVarious cleanup of the REPL, mainly with parsing and completion IBC.hsIBC generation pattern match completeness IdeMode.hsAdd IDE command to get Idris version IdrisDoc.hsPlumb source locations through Tactical's elab Imports.hsAdd function to list installed packages Inliner.hs Interactive.hsRename ideslave to ide-mode Output.hsCatch some lingering renames that I missed ParseData.hsSupport type errors in docstrings ParseExpr.hsDesugar do blocks inside of %runTactics ParseHelpers.hsExpose equality proofs in with rule ParseOps.hsMerge branch 'master' of github.com:markuspf/Idris-dev into markuspf-master Parser.hsExpose equality proofs in with rule PartialEval.hsAdd scoped implicit argument to Pi Primitives.hsIO primitives tweak to support JS ProofSearch.hsIO primitives tweak to support JS Prover.hsCatch some lingering renames that I missed Providers.hsAnnotate several top-level functions REPL.hsAdd IDE command to get Idris version REPLParser.hsVarious cleanup of the REPL, mainly with parsing and completion Transforms.hsFix for name clashes when applying transformations TypeSearch.hsIgnore lazy type modifiers in :search Unlit.hsAdded TODOs for Unlit.hs WhoCalls.hsMark 'case' on unique types as updatable