git.iko.soy/Idris-dev
on 2aaff41 help sign in
Idris-dev/src/Idris
2 folders, 46 files
../ Core/Stop erasing binder types in executor Elab/Fix parameter identification ASTUtils.hsTidy up the IState when classes are undefined AbsSyntax.hsStore parameters in function types AbsSyntaxTree.hsStore parameters in function types Apropos.hs:apropos syntax for binders CaseSplit.hsDon't update after '?' when case splitting Chaser.hsBring module loading into Idris monad CmdOptions.hsDocument --check in --help Colours.hsAdd semantic highlighting for postulates Completion.hsFinal cleanup/check of case tactic implementation Coverage.hsDisable old productivity checker DSL.hsKeep type arguments of = when unelaborating DataOpts.hsRemove collapsibility and forceability altogether. DeepSeq.hsAdd tactics "skip" and "fail" Delaborate.hsSpot name clases in error messages Docs.hsMerge branch 'master' into parenthasizeInfix Docstrings.hsEnable word-wrapping in docstrings ElabDecls.hsAdded idris-c executable ElabQuasiquote.hsKeep type arguments of = when unelaborating ElabTerm.hsMore efficiency improvements Erasure.hsMerge remote-tracking branch 'upstream/master' into cantResolveAlts ErrReverse.hsFix for matchProblems Error.hsRemove all the handle arguments Help.hsAdded :let and :undefine to the repl help IBC.hsStore parameters in function types IdeSlave.hsmove getNChar and getLen to IdeSlave IdrisDoc.hsKeep type arguments of = when unelaborating Imports.hsSupport builds that doesn't use cabal for libs and rts Inliner.hsAdd a Cabal library Interactive.hsTake .lidr syntax into account with :addmissing Output.hsAdding a prettyprinted message for undefining names ParseData.hsMerge branch 'master' of https://github.com/idris-lang/Idris-dev into feature/casetactic ParseExpr.hsAllow “!” to start a larger operator ParseHelpers.hsRemove all the handle arguments ParseOps.hsKeep type arguments of = when unelaborating Parser.hsUse strings for code generators PartialEval.hsAdded some additional documentation for partial evaluation Primitives.hsAdd a prim__systemInfo primitive. ProofSearch.hsAdd an optional depth to 'search' tactic Prover.hsStop encoding prover messages as output Providers.hsDistinguish postulate providers and type providers at use site REPL.hsStore parameters in function types REPLParser.hsInvoke external code generator Transforms.hsUse Data.Text for variable names TypeSearch.hsRemove all the handle arguments Unlit.hsPrepared data structure of FC for spanning, and added the span of the last token parsed to Idris WhoCalls.hsAdd :who-calls and :calls-who to IDESlave