1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Inductive Num : Type :=
| pos :> Pos -> Num
| neg :> Neg -> Num
with Pos : Type :=
| a : Pos
with Neg : Type :=
| b : Neg.
Definition name (x : Num) : nat :=
match x with
| a => 0
| b => 1
end.
(* Note that the following should be accepted but is not. The reason
it that it is assumed that the first line is irrefutable so that
the split on a and b in the first row is dropped. *)
Fail Check fun x y : Num => match x, y with
| x, a => 0
| a, b => 1
| b, b => 2
end.
|
