blob: dfc8c328064e74aee52597e3fa34e5fa1d83e652 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
Inductive I : Set :=
| A : nat -> nat -> I
| B : nat -> nat -> I.
Definition foo1 (x:I) : nat :=
match x with
| A a b | B a b => S b
end.
Definition foo2 (x:I) : nat :=
match x with
| A _ b | B b _ => S b
end.
Definition foo (x:I) : nat :=
match x with
| A a b | B b a => S b
end.
|
