on 6faa1ab help sign in
Idris-dev/src/Idris
2 folders, 46 files
../ Core/Add annotations for :search result classification Elab/Use exact name lookup when building from ibc ASTUtils.hsTidy up the IState when classes are undefined AbsSyntax.hsEitherErr Applicative for Functor-Applicative-Monad_Proposal AbsSyntaxTree.hsRenaming of built-in datatypes works finally Apropos.hsFirst renaming attempt CaseSplit.hsAnnotate several top-level functions Chaser.hsBring module loading into Idris monad CmdOptions.hsFix typo in help message (language extension) Colours.hsAdd semantic highlighting for postulates Completion.hsAdd completion support for newer command arg types Coverage.hsUse exact name lookup when building from ibc DSL.hsKeep type arguments of = when unelaborating DataOpts.hsCache uniqueness information in NameType DeepSeq.hsEXPERIMENTAL uniqueness types Delaborate.hsStore kind in Pi binders Docs.hsMerge branch 'master' into parenthasizeInfix Docstrings.hsEnable word-wrapping in docstrings ElabDecls.hsRenaming of built-in datatypes works finally ElabQuasiquote.hsKeep type arguments of = when unelaborating ElabTerm.hsRenaming of built-in datatypes works finally Erasure.hsFirst renaming attempt ErrReverse.hsFix for matchProblems Error.hsError when using empty namespace for disambiguation at REPL Help.hsAdd :printdef command to show the definition of a pattern-matching operation IBC.hsUse exact name lookup when building from ibc IdeSlave.hsIDE support for :printdef IdrisDoc.hsKeep type arguments of = when unelaborating Imports.hsSupport builds that doesn't use cabal for libs and rts Inliner.hs Interactive.hsStore kind in Pi binders Output.hsNew command :pprint for outputting paper/slide bits ParseData.hsMerge branch 'master' of https://github.com/idris-lang/Idris-dev into feature/casetactic ParseExpr.hsFirst renaming attempt ParseHelpers.hsRemove all the handle arguments ParseOps.hsMerge branch 'master' of github.com:markuspf/Idris-dev into markuspf-master Parser.hsUse strings for code generators PartialEval.hsAnnotate several top-level functions Primitives.hsRename float negation primitive for more uniformity ProofSearch.hsEXPERIMENTAL uniqueness types Prover.hsMake output from :t name annotate with terms Providers.hsAnnotate several top-level functions REPL.hsNew command :pprint for outputting paper/slide bits REPLParser.hsNew command :pprint for outputting paper/slide bits Transforms.hsMark 'case' on unique types as updatable TypeSearch.hsAdd annotations for :search result classification Unlit.hsPrepared data structure of FC for spanning, and added the span of the last token parsed to Idris WhoCalls.hsMark 'case' on unique types as updatable