blob: 378859e98cd922ad3d11951b76c978254c982e96 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
(* ============================================== *)
(* To test compilation of dependent case *)
(* Multiple Patterns *)
(* ============================================== *)
Inductive skel : Type :=
| PROP : skel
| PROD : skel -> skel -> skel.
Parameter Can : skel -> Type.
Parameter default_can : forall s : skel, Can s.
Type
(fun s1 s2 : skel =>
match s1, s2 return (Can s1) with
| PROP, PROP => default_can PROP
| s1, _ => default_can s1
end).
Type
(fun s1 s2 : skel =>
match s1, s2 return (Can s1) with
| PROP, PROP => default_can PROP
| PROP as s, _ => default_can s
| PROD s1 s2 as s, PROP => default_can s
| PROD s1 s2 as s, _ => default_can s
end).
|
