git.iko.soy/Idris-dev
on 4e4b7df help sign in
history ofsrc/Idris/Coverage.hs
all commits
749eceePerform positivity checking for Elab-defined datatypesDavid Christiansen 2392716Fix silly error in totality checkerEdwin Brady cfc8436Don't normalise constructor typesEdwin Brady 9f202dcMake coverage checking more conservativeEdwin Brady 6c682f3Comment editingEdwin Brady 6efe40bExtend rules for 'impossible' casesEdwin Brady d3dc418Add names in types to call graphEdwin Brady 0175376Remove some unnecessary fieldsEdwin Brady 39a8c78Categorised the Logs.Jan de Muijnck-Hughes 9f3675aStore patvar binding types in idris_patdefsShea Levy 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