git.iko.soy/Idris-dev
on 194c86b help sign in
194c86bCorrect Semilattice ImplementationsSam Elliott 29c02f4Fix scope/matching issues in proof scriptsEdwin Brady 8ed343bRemove dodgy unification hackEdwin Brady b7756f2Merge pull request #1380 from david-christiansen/no-trace-on-withDavid Christiansen ec228a0Merge pull request #1377 from puffnfresh/missing-instancesDavid Christiansen cfc2386Merge pull request #1379 from david-christiansen/paren-S-patDavid Christiansen 1cdd0dfDon't do trace when `with` doesn't matchDavid Raymond Christiansen 72f7b58Add parens on generated S patternsDavid Raymond Christiansen adba5beAdd Ord instance for BoolBrian McKenna 5b723cbMerge pull request #1376 from Melvar/ideslave-letDavid Christiansen ab1fbfeAllow :let in ideslaveMelvar Chen 330eaa5Merge pull request #1375 from david-christiansen/type-search-in-proverDavid Christiansen 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 e6bec02Fix parameter propagation on CAFsEdwin Brady 6c39e35Fix parameter expansion in PEq caseEdwin Brady ecc5277Remove commented out codeEdwin Brady ecb9da6Support multiple let bindingsEdwin Brady 1269791Keep type arguments of = when unelaboratingEdwin Brady 3a2c8aaMake prover better at IDESlave protocolDavid Raymond Christiansen f0ba64cMerge pull request #1369 from david-christiansen/prover-output-colorEdwin Brady f05e088Merge pull request #1368 from Heather/cleanEdwin Brady 9af885aHighlight differing implicits in errorsEdwin Brady f5c6883Update CHANGELOG for unbound implicitsEdwin Brady e336883Highlight prover output for ideslaveDavid Raymond Christiansen 24acd05windows executables should end with .exeHeather 32d47a5Ensure erasure happens under 'force'Edwin Brady 6f6a167No need for 'using' in HVectEdwin Brady 505905dRemove some needless 'using' blocksEdwin Brady 99ebe20Merge pull request #1364 from puffnfresh/neweffects-bad-constraintsEdwin Brady 2d41378Merge pull request #1363 from bmsherman/parseDefEdwin Brady 5ffef89Type class resolution fixEdwin Brady e363c09Better treatment of unbound implicitsEdwin Brady 8279c80Remove bad Applicative constraints from neweffectsBrian McKenna fc5a9cbFix parser for :def REPL commandbmsherman 3c4bd14Merge pull request #1361 from trillioneyes/repl-definitionsEdwin Brady d9513aaMerge pull request #1360 from ziman/case-elab-erasureEdwin Brady cefb325Merge pull request #1358 from ahmadsalim/documentation/partialevaluationEdwin Brady 61f3456Simplify argsToAlt.Matus Tejiscak 98352eeComment clarification.Matus Tejiscak 019b608Purify toPats.Matus Tejiscak 15b9807Disable PAny for repeated patvars.Matus Tejiscak 2490a15Implement accessible+inaccessible splitting.Matus Tejiscak 1e37348More changes to argsToAlt.Matus Tejiscak 2cc6526Adjust code around argsToAlt.Matus Tejiscak 747aaf5Extend argsToAlt to return a quadruple.Matus Tejiscak 204ebf5Added support for data definitionsAlyssa Carter bfdec8fRemoved some commented-out codeAlyssa Carter c1277c8Handling more forms of definition.Alyssa Carter