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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
Set Implicit Arguments.
Definition err : Type := unit.
Inductive res (A: Type) : Type :=
| OK: A -> res A
| Error: err -> res A.
Arguments Error [A].
Set Printing Universes.
Section FOO.
Inductive ftyp : Type :=
| Funit : ftyp
| Ffun : list ftyp -> ftyp
| Fref : area -> ftyp
with area : Type :=
| Stored : ftyp -> area
.
Print ftyp.
(* yields:
Inductive ftyp : Type (* Top.27429 *) :=
Funit : ftyp | Ffun : list ftyp -> ftyp | Fref : area -> ftyp
with area : Type (* Set *) := Stored : ftyp -> area
*)
Fixpoint tc_wf_type (ftype: ftyp) {struct ftype}: res unit :=
match ftype with
| Funit => OK tt
| Ffun args =>
((fix tc_wf_types (ftypes: list ftyp){struct ftypes}: res unit :=
match ftypes with
| nil => OK tt
| cons t ts =>
match tc_wf_type t with
| OK tt => tc_wf_types ts
| Error m => Error m
end
end) args)
| Fref a => tc_wf_area a
end
with tc_wf_area (ar:area): res unit :=
match ar with
| Stored c => tc_wf_type c
end.
End FOO.
Print ftyp.
(* yields:
Inductive ftyp : Type (* Top.27465 *) :=
Funit : ftyp | Ffun : list ftyp -> ftyp | Fref : area -> ftyp
with area : Set := Stored : ftyp -> area
*)
Fixpoint tc_wf_type' (ftype: ftyp) {struct ftype}: res unit :=
match ftype with
| Funit => OK tt
| Ffun args =>
((fix tc_wf_types (ftypes: list ftyp){struct ftypes}: res unit :=
match ftypes with
| nil => OK tt
| cons t ts =>
match tc_wf_type' t with
| OK tt => tc_wf_types ts
| Error m => Error m
end
end) args)
| Fref a => tc_wf_area' a
end
with tc_wf_area' (ar:area): res unit :=
match ar with
| Stored c => tc_wf_type' c
end.
(* yields:
Error:
Incorrect elimination of "ar" in the inductive type "area":
the return type has sort "Type (* max(Set, Top.27424) *)" while it
should be "Prop" or "Set".
Elimination of an inductive object of sort Set
is not allowed on a predicate in sort Type
because strong elimination on non-small inductive types leads to paradoxes.
*)
|
