aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/Case3.v
blob: eaafd41fa8c1199071d8134a89da31a50c951a82 (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.

Fail Type
  (fun l : List nat =>
   match l return nat with
   | Nil nat => 0
   | Cons a l => S a
   end).