diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-24 17:38:09 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-24 17:45:18 +0200 |
| commit | 9420069e4d0bf3bf377c950bbc41ea762fbcfce8 (patch) | |
| tree | c167f8509aad7458fb56672da586156e6200bd32 /kernel/declareops.ml | |
| parent | f7f5b7dcc641e233a1b18dab7228d1d8c55596b3 (diff) | |
Extend test-suite for the positivity checker.
I wasn't very creative: I just added a single test by failure case in the positivity checker (plus one success).
There should probably be tests with mutually inductives and co-inductives as well.
Diffstat (limited to 'kernel/declareops.ml')
0 files changed, 0 insertions, 0 deletions