on 8935fed help sign in
all commits
673a1fcTweak for types of case blocksEdwin Brady d6458bbAdd `{n} for quotations of the global name nDavid Raymond Christiansen e0b0516Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 53d5548Merge pull request #2167 from david-christiansen/bump-pprint-boundDavid Christiansen f238715Remove unused Show instanceDavid Raymond Christiansen ab9a2bcAdd a :browse command to the REPL and IDE equivalentDavid Raymond Christiansen d97715ePlumb datatype information through the proof stateDavid Raymond Christiansen 370939bMerge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady f987aecAdd info field to AppEdwin Brady 31f4c82Pretty-print bindings of MNs the same as references to MNsDavid Raymond Christiansen f1c6e39Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 7a8217aUse Set for boundNamesInEdwin Brady c3def79Rename Tactical to ElabDavid Raymond Christiansen 7d02904Progress towards defining functions in TacticalDavid Raymond Christiansen da8b88ashow incomplete term holes for listy constructorsJP Smith 5d269e3:exec can take an expression as an argumentEdwin Brady 5804426Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 0f86748Fix build errors with GHC 7.10.1. Fixes #2080Jan Stolarek 13a36a3Annotate functions as %hint for auto searchEdwin Brady fc02362Support externally defined primitivesEdwin Brady d57d60aUse a Set for universe constraintsEdwin Brady 174395bMerge remote-tracking branch 'upstream/master' into issue2004Andreas Reuleaux 15737d9Trickiness with implicits in dependent classesEdwin Brady aa33865Merge remote-tracking branch 'upstream/master' into issue2004Andreas Reuleaux 1bf2731issue #2004 resolved by --consolewith cmd line paramAndreas Reuleaux 6d188c4Begin to use a sum type for post-elab IState tweaksDavid Raymond Christiansen 361efb5Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 147149bAdd 'determining parameters' for classesEdwin Brady c2dc6ecAllow new-style tactics to declare function signaturesDavid Raymond Christiansen 75f6c2dAdd :core to the REPLDavid Raymond Christiansen bb013f0Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen 3d87454TT pretty-printing - also in elab debugDavid Raymond Christiansen 6fe15eaAllow type providers to have docstringsAdam Sandberg Eriksson 7ba4da0Instance docs: instance parameter documentationAdam Sandberg Eriksson 5ca59efInstance docs: haddocks grammarAdam Sandberg Eriksson 2d205a6Instance docs: basic plumbing of types and parsingAdam Sandberg Eriksson d4371e6Generate interface files for C->Idris callsEdwin Brady f7648dbForeign export lists in IOEdwin Brady 83793a6Add the ability for IDEs to get documentation overviewsDavid Raymond Christiansen 4d16a95Changed desugaring behavior to use <*> instead of <$>Tenor Biel 2758aaeMerge branch 'wip/tactical' of https://github.com/david-christiansen/Idris-dev into david-christiansen-wip/tacticalEdwin Brady 13e8ad8Plumb source locations through Tactical's elabDavid Raymond Christiansen 4d1759ePair syntax for unique typesEdwin Brady a0346b6Begin implementation of reflected elab monadDavid Raymond Christiansen f17606a"claim" and "unfocus" tacticsDavid Raymond Christiansen 40d094dExpose equality proofs in with ruleEdwin Brady c918f44Merge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady 26cfbe9Scoped implicits fixEdwin Brady b85b2ebRename ideslave to ide-modeDavid Raymond Christiansen a87f69eMerge pull request #1885 from david-christiansen/issue/1860David Christiansen