git.iko.soy/Idris-dev
on ced7733 help sign in
ced7733Replace 'effects' with neweffectsEdwin Brady 6e39ba5Normalise everything before 'with' abstractionEdwin Brady 1d23ad1Normalise before abstracting over 'with' typeEdwin Brady 4d62d30x = y now tries homogeneous equality firstEdwin Brady 228877aMerge pull request #1392 from ziman/fix-dctor-erasureEdwin Brady 25de16dDisjoint constants should be fatal in unificationEdwin Brady c1968edFix parameter spotting in function typesEdwin Brady 4ca8e46Fix data ctor arity comparison.Matus Tejiscak adb59d0Resolve class instances under let bindingsEdwin Brady 0a1965eChange 'Not a guess' errorEdwin Brady 82753c9Merge pull request #1387 from raichoo/javascriptraichoo 8915184javascript: wrap exceptions in functionraichoo 6f23501javascript: whitespaceraichoo a50224djavascript: factor AST into own moduleraichoo f9f43c4Merge pull request #1385 from raichoo/javascriptraichoo b669628javascript: switch to Data.Text for code generationraichoo 5277735Merge pull request #1383 from david-christiansen/issue/1337David Christiansen a430c3eMerge pull request #1382 from david-christiansen/incomplete-quasiquoteDavid Christiansen 72cddc6Generate legal names for infix op lemmasDavid Raymond Christiansen 90bb76dRemove unused codeDavid Raymond Christiansen 9cd2dfbUpdate tests for rechecking of quasiquotesDavid Raymond Christiansen d5411e2Recheck quasiquotesDavid Raymond Christiansen 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