git.iko.soy/Idris-dev
on 30585fc help sign in
Idris-dev/src/Idris
3 folders, 47 files
../ Core/Proof search should only use user visible names Elab/Merge remote-tracking branch 'upstream/master' into wip/tactical REPL/Only show accessible names in :browse ASTUtils.hsAdd export lists AbsSyntax.hsProof search should only use user visible names AbsSyntaxTree.hsDisplay tweak 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.hsCheck if existing IBC file has old version in Chaser.hs CmdOptions.hsPass parameters to codegens with new cmdoption --cg-opt Colours.hsIndicate the end of each escape sequence in the prompt string, since there's no way for Haskeline to detect it automatically. Completion.hsProof search should only use user visible names Coverage.hsMerge remote-tracking branch 'upstream/master' into parser-highlights DSL.hsSemantic highlighting of implicit fromInteger DataOpts.hsAdd export lists DeepSeq.hsProof search should only use user visible names Delaborate.hsProof search should only use user visible names Directives.hsHighlight names in directives Docs.hsAdd extra HL information to PRef Docstrings.hsAnnotate links with their URL ElabDecls.hsAllow mutually recursive records ElabQuasiquote.hsSemantic highlighting of implicit fromInteger Erasure.hsFix erasure from mkForeignPrim. ErrReverse.hsAdd export lists Error.hsSemantic highlighting of implicit fromInteger Help.hsDisplay 'Hole' instead of 'Metavariable' IBC.hsProof search should only use user visible names IdeMode.hsAdd :makecase (:mc) to REPL and ide-mode IdrisDoc.hsProof search should only use user visible names Imports.hsAdd export lists Inliner.hsAdd export lists Interactive.hsVariable names in makelemma types Output.hsParser-driven highlighting of quasiquoted regions ParseData.hsMultiple record fields on one line (#2460) ParseExpr.hsProof search should only use user visible names ParseHelpers.hsRevert "Allow an optional trailing comma in `commaSeparated`" ParseOps.hsAdd extra HL information to PRef Parser.hsHighlight all keywords with the parser PartialEval.hsAdd extra HL information to PRef Primitives.hsFix totality of chr ProofSearch.hsSlightly relax check for proofsearchability Prover.hsAdd extra HL information to PRef Providers.hsAdd extra HL information to PRef REPL.hsProof search should only use user visible names REPLParser.hsAdd :makecase (:mc) to REPL and ide-mode Reflection.hsMerge remote-tracking branch 'upstream/master' into wip/tactical 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