git.iko.soy/Idris-dev
on cf47310 help sign in
Idris-dev/src/Idris
3 folders, 47 files
../ Core/Use subst for intro, rather than updsubst Elab/Insert namespace information to declaration-level %runElab REPL/Only show accessible names in :browse ASTUtils.hsAdd export lists AbsSyntax.hsProof search should only use user visible names AbsSyntaxTree.hsSome display tweaks for explicit arguments 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.hs(Temporary) remove hasValidIBCVersion check CmdOptions.hsPass parameters to codegens with new cmdoption --cg-opt Colours.hsExperimental support for console colours on Windows Completion.hsProof search should only use user visible names Coverage.hsFix coverage checker for sigma types DSL.hsSemantic highlighting of implicit fromInteger DataOpts.hsAdd export lists DeepSeq.hsInsert namespace information to declaration-level %runElab Delaborate.hsSome display tweaks for explicit arguments Directives.hsHighlight names in directives Docs.hsAdd extra HL information to PRef 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.hsSemantic highlighting of implicit fromInteger Help.hsDisplay 'Hole' instead of 'Metavariable' IBC.hsInsert namespace information to declaration-level %runElab 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.hsSome display tweaks for explicit arguments Output.hsExperimental support for console colours on Windows ParseData.hsMultiple record fields on one line (#2460) ParseExpr.hsAllow syntax rules at the declaration level ParseHelpers.hsBetter failure on indentation stack underflow ParseOps.hsAdd extra HL information to PRef Parser.hsInsert namespace information to declaration-level %runElab PartialEval.hsAdd extra HL information to PRef Primitives.hsFix totality of chr ProofSearch.hsSlight relaxation of proof search rules Prover.hsShow MNs that occur in the goal in the interactive provers Providers.hsAdd extra HL information to PRef REPL.hsCheck for TTY when setting colour REPLParser.hsAdd :makecase (:mc) to REPL and ide-mode Reflection.hsLook up operator fixity in Elab 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