git.iko.soy/Idris-dev
on da672ec help sign in
history ofsrc/Idris/Coverage.hs
all commits
83f0af1Display expected type of RHS in error messagesEdwin Brady fcba396Coverage checker fixEdwin Brady 3288a6cFix coverage checker for sigma typesEdwin Brady bc2915cMerge remote-tracking branch 'upstream/master' into parser-highlightsDavid Raymond Christiansen 5da0d60Faster processing of alternativesEdwin Brady a54852bHighlighting for pairs, lists and sigmasDavid Raymond Christiansen 3cd25e6Add extra HL information to PRefDavid Raymond Christiansen 4dabdbaPropagate errors originating from case treesDavid Raymond Christiansen 73b666bMerge remote-tracking branch 'refs/remotes/upstream/master' into name-highlightsDavid Raymond Christiansen 74fd10aFix 'impossible' checkEdwin Brady c46243bInitial implementation of semantic editor hightlightingDavid Raymond Christiansen c56dee3Wrap data declarations in mutual blocksDavid Raymond Christiansen 04b4cc0Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tacticalDavid Raymond Christiansen e32e899Totality checking for functions defined in Elab scriptsDavid Raymond Christiansen f987aecAdd info field to AppEdwin Brady 15737d9Trickiness with implicits in dependent classesEdwin Brady e0dc91eMake some comments into proper HaddockDavid Raymond Christiansen df574ecRemember full names when checking impossible patternsDavid Raymond Christiansen 17fe233Add scoped implicit argument to PiEdwin Brady 4175a7fCoverage checker should ignore hidden argumentsEdwin Brady 4c16335Coverage checker fix for nested constantsEdwin Brady 8cbdc83Look in binders when building size change graphEdwin Brady 6c0b2b9Lifted TODO/Fixme from Coverage checker.Jan de Muijnck-Hughes 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