blob: 87431a75c7e61a28a3f08a5ce43353ea4b00f27e (
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
|
(* Check local definitions in context of inductive types *)
Inductive A [C,D:Prop; E:=C; F:=D; x,y:E->F] : E -> Set :=
I : (z:E)(A C D x y z).
Check
[C,D:Prop; E:=C; F:=D; x,y:(E ->F);
P:((c:C)(A C D x y c) ->Type);
f:((z:C)(P z (I C D x y z)));
y0:C; a:(A C D x y y0)]
<[y1:C; a0:(A C D x y y1)](P y1 a0)>Cases a of (I x0) => (f x0) end.
Record B [C,D:Set; E:=C; F:=D; x,y:E->F] : Set := { p : C; q : E }.
Check
[C,D:Set; E:=C; F:=D; x,y:(E ->F);
P:((B C D x y) ->Type);
f:((p0,q0:C)(P (Build_B C D x y p0 q0)));
b:(B C D x y)]
<[b0:(B C D x y)](P b0)>Cases b of (Build_B x0 x1) => (f x0 x1) end.
(* Check implicit parameters of inductive types (submitted by Pierre
Casteran and also implicit in #338) *)
Set Implicit Arguments.
CoInductive LList [A:Set] : Set :=
| LNil : (LList A)
| LCons : A -> (LList A) -> (LList A).
Implicits LNil [1].
Inductive Finite [A:Set] : (LList A) -> Prop :=
| Finite_LNil : (Finite LNil)
| Finite_LCons : (a:A) (l:(LList A)) (Finite l) -> (Finite (LCons a l)).
|
