test-suite/failure/Case3.v


1
2
3
4
5
6
7

Inductive List [A:Set] :Set := 
 Nil:(List A) | Cons:A->(List A)->(List A).

Type [l:(List nat)]<nat>Cases l of 
                         (Nil nat) =>O
                      | (Cons  a l) => (S a)
                      end.