on 4e69658 help sign in
all commits
f664681Productivity checker tweakEdwin Brady 08cef17HLint DIrected Code CleanupJan de Muijnck-Hughes 4c83174Totality checker mutual fixEdwin Brady 9f55048Look under if...then...else in totality checkerEdwin Brady b03f823Fix evaluation of InfEdwin Brady 8b1502aGenerate cases for coverage from 'impossible'Edwin Brady 0896073Added documentation for modules.Jan de Muijnck-Hughes 2cfcbcfPositivity checking under parametersEdwin Brady 1019ce5Source file stylings & Haddock.Jan de Muijnck-Hughes 536372fRename Lazy' => DelayedEdwin Brady 57136ccChange elaboration of interfacesEdwin Brady fe1d470Totality checking now looks inside case directlyEdwin Brady 85d4b4eImprove productivity checkEdwin Brady 1d0e33cRemove a "can't happen" errorEdwin Brady c931e38Use exact lookup in size-change checkingEdwin Brady 5134aebBetter support for mutually defined typesEdwin Brady faa58adFix evaluation of non-total thingsEdwin Brady 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