on 73da7d4 help sign in
all commits
aa33865Merge remote-tracking branch 'upstream/master' into issue2004Andreas Reuleaux 1bf2731issue #2004 resolved by --consolewith cmd line paramAndreas Reuleaux 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 914d992Bound the depth of hole searchingDavid Raymond Christiansen b8abab8Always show holes when pretty-printing delaborationsDavid Raymond Christiansen 4d8ab37Allow identifiers to start with underscore (_). Fixes idris-lang/Idris-dev#1868Ahmad Salim Al-Sibahi 8096500Add %used pragmaEdwin Brady 3c187ceBetter tracking of FC in implicit coercions / DSLDavid Raymond Christiansen 60e4921Relax lower bound on mtlEric Mertens 02d26ecMerge pull request #1841 from david-christiansen/issue/1806David Christiansen c729d2fSupport scoped type class constraintsEdwin Brady e0cab49Allow implicits to appear anywhereEdwin Brady 0b23ef2Replace _ patterns with fresh variables under @-patternsDavid Raymond Christiansen 17fe233Add scoped implicit argument to PiEdwin Brady 0a1b72cMerge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady cad3b02Eat less memory by sharing namesEdwin Brady 6b803b7Allow documentation for modulesDavid Raymond Christiansen c1cf03fMerge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady 2ec25c2Do more forcing in IBCEdwin Brady ec2b304Extended OptNorbert Melzer 7c34217Allow class constraints to be namedEdwin Brady ee32989Search in current elaboration stack for instancesEdwin Brady ab32c46Merge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady 02a36adAllow :search and :apropos to search packagesEdwin Brady 26da5c7Save index file when installing a packageEdwin Brady 96d370eFlip operator precedence rules for pretty-printingBen Sherman e95c877Make pattern matching consistent in lambda/letEdwin Brady