git.iko.soy/Idris-dev
on 7afa310 help sign in
history ofsrc/Idris/Coverage.hs
all commits
37748ceAdd transformation rules for partial evaluationEdwin Brady 323a109Use exact name lookup when building from ibcEdwin Brady 971d88dAnnotate several top-level functionsMichael Maloney 7e7368dStore kind in Pi bindersEdwin Brady 9abbc3fCache uniqueness information in NameTypeEdwin Brady f158123Disable old productivity checkerEdwin Brady c201192Bring erasure info to the case tree builder.Matus Tejiscak 5aa2a8eFind negative occurrences in positivity checkerEdwin Brady 7e78f0aExtend positivity check for mutual data typesEdwin Brady 5ba96c1Effect handlers should be coveringEdwin Brady 7143962Make totality a warning until compilingDavid Raymond Christiansen 4be2fbaAllow second argument of assert_smaller to be of different type than first argument since this could be useful for functions that are written with Universe-style pattern matching, i.e., where the rhs pattern has different type than the lhs expression.Ahmad Salim Al-Sibahi bfc3c3eMerge branch 'master' of github.com:edwinb/Idris-dev into default-arg-substTimo Petteri Sinnemäki c78fb14Fixed errors; partially complete default arg subsTimo Petteri Sinnemäki 06e2b1dEfficiency of coverage checkEdwin Brady d3eb486First attempt now at substitution to default argsTimo Petteri Sinnemäki fb6a0edCoverage checker fixEdwin Brady f0a5442Provide IDESlave output with docs and typeDavid Raymond Christiansen 9c99a07Add 'covering' function optionEdwin Brady 678fc86Finish guardedness checkEdwin Brady b0720b0Change guardedness check for new-style coinductionEdwin Brady 88aa6d1Support mixed induction/coinduction with Inf typeEdwin Brady 3cef609Annotate 'Lazy' with reason for lazinessEdwin Brady 7f3d436Remove some commented out codeEdwin Brady c1ef938New syntax for documentation commentsDavid Raymond Christiansen 130f437Remove | annotation, make Force/Delay implicitEdwin Brady f6bebd3Proper pretty-printing of dependent pairsDavid Raymond Christiansen e80f871Annotate and colour pairs and () properlyDavid Raymond Christiansen 6eee6c8Add assert_total functionEdwin Brady 526cd75Add assert_smaller functionEdwin Brady c0cc1ddMerge remote-tracking branch 'upstream/master' into semantic-pprintDavid Raymond Christiansen dc4ce0cReplace the string-slinging show with pretty-printDavid Raymond Christiansen fe3f03fAdded %error_reverse annotationEdwin Brady 803194fArgument options (instead of just a Bool for lazy)Edwin Brady d82f5feMerge branch 'text-names'Edwin Brady 0c8c90dStrictness annotationsEdwin Brady 46e894dUse Data.Text for variable namesEdwin Brady 7604451Cache argument types for building case treesEdwin Brady 3eb8fc8Fix earlier %assert_total propagationEdwin Brady 3985f42Propagate assert_total to case blocksEdwin Brady 67da31aMerge branch 'master' into cabal-libraryBrian McKenna 65c301cRecursive constructor disjointness + cleanupMatus Tejiscak 0f97368Merge branch 'master' into cabal-libraryBrian McKenna 5000aebAdd a Cabal libraryBrian McKenna 40e6293Some interactive editing fixesEdwin Brady 58a12c1Totality checker improvements (soundness)Edwin Brady ec3daa4Make sure deferred definitions get totality checkedEdwin Brady 3c32b65Whitespace cleanup.George Leontiev 76722bfRemove forcing optimisation from coverage checkerEdwin Brady 0e76ac9Remember whether implicits are machine generatedEdwin Brady