git.iko.soy/Idris-dev
on adbe613 help sign in
history ofsrc/Idris/Coverage.hs
all commits
5a6299bUnification fix Specifically to stop it filling in things which are given by the programmer (caused by a bug replacing nullary constructors with terms!)Edwin Brady 8063cfdAdded --dumpcases <file> option for dumping case trees on compilingEdwin Brady 489ea6fPass pattern variable names to match compilerEdwin Brady dc67893Remove some unused codeEdwin Brady 97e28f7Export tactic-implicit arguments properlyEdwin Brady 33baa44More on errors; propagate line numbersEdwin Brady ed72247Try to get line numbers betterEdwin Brady c7a3b59Coverage checker tweakEdwin Brady f49cd3bPass options on functions in typeclasses through to instancesEdwin Brady 9839562Fix silly error in termination checker :)Edwin Brady 7142d7eTotality checker tweaksEdwin Brady b1e95cbFix coverage checkerEdwin Brady 7fb7decImproved termination check (gets ackermann now, but still no mutual recursive definitions)Edwin Brady 98be75cAdded (experimentally) auto implicit argumentsEdwin Brady fc6eb53Bug fixes; checking type names in data declsEdwin Brady de6bb41Added 'total' keyword and positivity checkEdwin Brady ae4be75Well founded recursion checkEdwin Brady 1112fe4Coverage checker Not quite complete - a bug (which I know how to fix) makes some things appear not covering even though they are. Results currently used only for pruning case trees in compiled code. There is a small performance penalty - coverage checking can be disable with --nocoverageEdwin Brady 60c4ef9Added 'impossible' keywordEdwin Brady