on 7afa310 help sign in
all commits
98352eeComment clarification.Matus Tejiscak c1277c8Handling more forms of definition.Alyssa Carter c201192Bring erasure info to the case tree builder.Matus Tejiscak d8ed044Add getInaccessibleArgs.Matus Tejiscak a5e8ca3Changed :let to work with an arbitrary number of `PDecl`s (though only one name at a time for now).Alyssa Carter e260741Preliminary support for a :let command in the replAlyssa Carter dac312bAdd goal types to quasiquotes.David Raymond Christiansen e08a18dMerge remote-tracking branch 'refs/remotes/upstream/master' into quasiquoteDavid Raymond Christiansen c90d4b4Parsing for quasiquotesDavid Raymond Christiansen 67f7373Support builds that doesn't use cabal for libs and rtsniklas 48a9659fix spelling of "parenthesise"Ricky Elrod 22b2548Merge pull request #1323 from bmsherman/parenthasizeInfixDavid Christiansen c4eca4fMerge branch 'master' into parenthasizeInfixbmsherman 7d38943Proper and complete parenthasization of infix operator names.bmsherman fc6f5feMerge pull request #1322 from bmsherman/equalDeclDavid Christiansen c4ce749Parenthasize infix names in REPL outputbmsherman 802c248Make type arguments in (=) declaration implicit (for docs)bmsherman cebd1b4Merge pull request #1315 from david-christiansen/serialized-termsDavid Christiansen e245d48Maintain pretty-printer bound varsDavid Raymond Christiansen 80d1a88Fix implicit spotting in case blocksEdwin Brady d1a832aSend serialized versions of TT terms in pprintDavid Raymond Christiansen 4833cb3Merge branch 'master' of https://github.com/idris-lang/Idris-dev into feature/casetacticAhmad Salim Al-Sibahi 9993f3bAdd pi to overridable syntax in DSL blocksDavid Raymond Christiansen 5045daeAdded tactic for case analysis. Also, induction now work on expressions instead of simply names.Ahmad Salim Al-Sibahi a0b05e2Allow induction on terms instead of simply namesAhmad Salim Al-Sibahi baaea97Merge pull request #1288 from david-christiansen/issue/1286David Christiansen d6c5b2bAdd semantic highlighting for postulatesDavid Raymond Christiansen e5bc47eDistinguish postulate providers and type providers at use siteDavid Raymond Christiansen a75bd0fMerge pull request #1280 from david-christiansen/testrunnerEdwin Brady 10279e6Merge pull request #1276 from jfdm/warranty-flagEdwin Brady 3b37dafMerge pull request #1265 from ziman/dependent-pairsEdwin Brady e2a34a8Add --testpkg option + tests section in IPKG filesDavid Raymond Christiansen fdb79e6Added warranty information to the Idris Repl.Jan de Muijnck-Hughes 9c3fefeImprove appearance of type search results.bmsherman 42c28d2Rename Pair to Sigma.Matus Tejiscak 5c4ee75Make load to line work with mutual blocksEdwin Brady 7e78f0aExtend positivity check for mutual data typesEdwin Brady e541d7eReorganise dependent pair types in Prelude.Matus Tejiscak e7a35e9Remove implicit qualifier for 'effect'Edwin Brady 94fc13cIDESlave support for :loadtoDavid Raymond Christiansen 602552eAdd :loadto commandEdwin Brady 094be98Add an optional depth to 'search' tacticEdwin Brady 8b55229Merge pull request #1222 from klrr/split-binsDavid Christiansen 9be5866started working on new cmd arg parserklrr 719d472'search' now fails if there are metavariablesEdwin Brady af99a9dAdd :makelemma command in interactive editingEdwin Brady e1f7597Merge pull request #1204 from david-christiansen/totality-warningEdwin Brady e16c068Documentation for primitivesDavid Raymond Christiansen 7143962Make totality a warning until compilingDavid Raymond Christiansen 89a975eImprove ideslave highlighting of primitivesDavid Raymond Christiansen