blob: 2294452001f097fd334615a73361281c1570dd57 (
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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
(* Check compilation of multiple pattern-matching on terms non
apparently of inductive type *)
(* Check that the non dependency in y is OK both in V7 and V8 *)
Check ([x;y:Prop;z]<[x][z]x=x \/ z=z>Cases x y z of
| O y z' => (or_introl ? (z'=z') (refl_equal ? O))
| _ y O => (or_intror ?? (refl_equal ? O))
| x y _ => (or_introl ?? (refl_equal ? x))
end).
(* Suggested by Pierre Letouzey (PR#207) *)
Inductive Boite : Set :=
boite : (b:bool)(if b then nat else nat*nat)->Boite.
Definition test := [B:Boite]<nat>Cases B of
(boite true n) => n
| (boite false (n,m)) => (plus n m)
end.
(* Check lazyness of compilation ... future work
Inductive I : Set := c : (b:bool)(if b then bool else nat)->I.
Check [x]
Cases x of
(c (true as y) (true as x)) => (if x then y else true)
| (c false O) => true | _ => false
end.
Check [x]
Cases x of
(c true true) => true
| (c false O) => true
| _ => false
end.
(* Devrait produire ceci mais trouver le type intermediaire est coton ! *)
Check
[x:I]
Cases x of
(c b y) =>
(<[b:bool](if b then bool else nat)->bool>if b
then [y](if y then true else false)
else [y]Cases y of
O => true
| (S _) => false
end y)
end.
*)
|
