on 68c519e help sign in
Idris-dev/src/Idris
3 folders, 47 files
../ Core/Convert comments in WHNF.hs to Haddock Elab/Cache information when module chasing REPL/Only show accessible names in :browse ASTUtils.hsAdd export lists AbsSyntax.hsMerge pull request #2634 from david-christiansen/namesInQQ AbsSyntaxTree.hsMerge remote-tracking branch 'upstream/master' into wip/tactical Apropos.hsFixes some string comparison that made sigma show incorrectly. Showing types of first component of sigma type. CaseSplit.hsAdd :makecase (:mc) to REPL and ide-mode Chaser.hsDetect cycles in imports CmdOptions.hsMake it possible to disable tactic deprecation Colours.hsExperimental support for console colours on Windows Completion.hsAdd desugarnats to completion Coverage.hsCoverage checker fix DSL.hsRemove NErased DataOpts.hsSimplify reflection and Raw DeepSeq.hsMerge remote-tracking branch 'upstream/master' into wip/tactical Delaborate.hsFriendlier error on proof search failure Directives.hsHighlight names in directives Docs.hsFix parameters documentation in the record's customized display Docstrings.hsAnnotate links with their URL ElabDecls.hsInsert namespace information to declaration-level %runElab ElabQuasiquote.hsSemantic highlighting of implicit fromInteger Erasure.hsFix erasure from mkForeignPrim. ErrReverse.hsAdd export lists Error.hsAdd raw name quotes Help.hsDisplay 'Hole' instead of 'Metavariable' IBC.hsFriendlier error on proof search failure IdeMode.hsAdd :makecase (:mc) to REPL and ide-mode IdrisDoc.hsImprove HTML generation for records documentation Imports.hsAdd export lists Inliner.hsAdd export lists Interactive.hsSome display tweaks for explicit arguments Output.hsExperimental support for console colours on Windows ParseData.hsAdd deprecation warning for %elim ParseExpr.hsMake it possible to disable tactic deprecation ParseHelpers.hsUpdate tests for proof deprecation ParseOps.hsAdd extra HL information to PRef Parser.hsInsert namespace information to declaration-level %runElab PartialEval.hsAdd extra HL information to PRef Primitives.hsSubstring as primitive ProofSearch.hsFriendlier error on proof search failure Prover.hsIn interactive elaborator, show all premises Providers.hsAdd extra HL information to PRef REPL.hsDetect cycles in imports REPLParser.hsAdd option to desugar nats in REPL output Reflection.hsRemove NErased Transforms.hsAdd info field to App TypeSearch.hsAllow Elab scripts to register type class instances Unlit.hsAdded TODOs for Unlit.hs WhoCalls.hsAdd info field to App