packages feed

idris-1.2.0: test/totality006/expected

totality006.idr:8:1-29:
  |
8 | prf Z     Z     Oh impossible
  | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Main.prf is not total as there are missing cases

totality006a.idr:11:21-30:
   |
11 | prf' (S _) (S _) Oh impossible
   |                     ~~~~~~~~~~
prf' (S _) (S _) Oh is a valid case

totality006b.idr:10:1-34:
   |
10 | blargh [] (y :: xs) so = absurd so
   | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
totality006b.blargh is not total as there are missing cases