summaryrefslogtreecommitdiff
path: root/test-suite/failure/Case6.v
blob: f588d275e6cb4c37a19a385c3bba34bb98697fdd (plain)
1
2
3
4
5
6
7
8
9
10
Inductive List [A:Set] :Set := 
 Nil:(List A) | Cons:A->(List A)->(List A).


Type <(List nat)>Cases (Nil nat) of 
                NIL   => NIL
              | (CONS _ _)  => NIL

              end.