git.iko.soy/Idris-dev
on ced7733 help sign in
history ofsrc/Idris/AbsSyntaxTree.hs
all commits
c1968edFix parameter spotting in function typesEdwin Brady 7d95becMake type search work in the proverDavid Raymond Christiansen 6340534Merge pull request #1371 from david-christiansen/prover-output-colorDavid Christiansen c29e746Allow :doc in proverDavid Raymond Christiansen 1269791Keep type arguments of = when unelaboratingEdwin Brady 9af885aHighlight differing implicits in errorsEdwin Brady e363c09Better treatment of unbound implicitsEdwin Brady 3c4bd14Merge pull request #1361 from trillioneyes/repl-definitionsEdwin Brady 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