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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
|
<?xml encoding="ISO-8859-1"?>
<!-- DTD FOR CIC OBJECTS: -->
<!-- CIC term declaration -->
<!ENTITY % term '(LAMBDA|CAST|PROD|REL|SORT|APPLY|VAR|META|IMPLICIT|CONST|
LETIN|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate)'>
<!-- CIC sorts -->
<!ENTITY % sort '(Prop|Set|Type)'>
<!-- CIC sequents -->
<!ENTITY % sequent '((Decl|Def|Hidden)*,Goal)'>
<!-- CIC objects: -->
<!ELEMENT ConstantType %term;>
<!ATTLIST ConstantType
name CDATA #REQUIRED
id ID #REQUIRED>
<!ELEMENT ConstantBody %term;>
<!ATTLIST ConstantBody
for CDATA #REQUIRED
params CDATA #REQUIRED
id ID #REQUIRED>
<!ELEMENT CurrentProof (Conjecture*,body)>
<!ATTLIST CurrentProof
of CDATA #REQUIRED
id ID #REQUIRED>
<!ELEMENT InductiveDefinition (InductiveType+)>
<!ATTLIST InductiveDefinition
noParams NMTOKEN #REQUIRED
params CDATA #REQUIRED
id ID #REQUIRED>
<!ELEMENT Variable (body?,type)>
<!ATTLIST Variable
name CDATA #REQUIRED
id ID #REQUIRED>
<!ELEMENT Sequent %sequent;>
<!ATTLIST Sequent
no NMTOKEN #REQUIRED
id ID #REQUIRED>
<!-- Elements used in CIC objects, which are not terms: -->
<!ELEMENT InductiveType (arity,Constructor*)>
<!ATTLIST InductiveType
name CDATA #REQUIRED
inductive (true|false) #REQUIRED>
<!ELEMENT Conjecture %sequent;>
<!ATTLIST Conjecture
no NMTOKEN #REQUIRED
id ID #REQUIRED>
<!ELEMENT Constructor %term;>
<!ATTLIST Constructor
name CDATA #REQUIRED>
<!ELEMENT Decl %term;>
<!ATTLIST Decl
name CDATA #IMPLIED
id ID #REQUIRED>
<!ELEMENT Def %term;>
<!ATTLIST Def
name CDATA #IMPLIED
id ID #REQUIRED>
<!ELEMENT Hidden EMPTY>
<!ATTLIST Hidden
id ID #REQUIRED>
<!ELEMENT Goal %term;>
<!-- CIC terms: -->
<!ELEMENT LAMBDA (decl*,target)>
<!ATTLIST LAMBDA
sort %sort; #REQUIRED>
<!ELEMENT LETIN (def*,target)>
<!ATTLIST LETIN
id ID #REQUIRED
sort %sort; #REQUIRED>
<!ELEMENT PROD (decl*,target)>
<!ATTLIST PROD
type %sort; #REQUIRED>
<!ELEMENT CAST (term,type)>
<!ATTLIST CAST
id ID #REQUIRED
sort %sort; #REQUIRED>
<!ELEMENT REL EMPTY>
<!ATTLIST REL
value NMTOKEN #REQUIRED
binder CDATA #REQUIRED
id ID #REQUIRED
idref IDREF #REQUIRED
sort %sort; #REQUIRED>
<!ELEMENT SORT EMPTY>
<!ATTLIST SORT
value CDATA #REQUIRED
id ID #REQUIRED>
<!ELEMENT APPLY (%term;)+>
<!ATTLIST APPLY
id ID #REQUIRED
sort %sort; #REQUIRED>
<!ELEMENT VAR EMPTY>
<!ATTLIST VAR
relUri CDATA #REQUIRED
id ID #REQUIRED
sort %sort; #REQUIRED>
<!-- The substitutions are ordered by increasing DeBrujin -->
<!-- index. An empty substitution means that that index is -->
<!-- not accessible. -->
<!ELEMENT META (substitution*)>
<!ATTLIST META
no NMTOKEN #REQUIRED
id ID #REQUIRED
sort %sort; #REQUIRED>
<!ELEMENT IMPLICIT EMPTY>
<!ATTLIST IMPLICIT
id ID #REQUIRED>
<!ELEMENT CONST EMPTY>
<!ATTLIST CONST
uri CDATA #REQUIRED
id ID #REQUIRED
sort %sort; #REQUIRED>
<!ELEMENT MUTIND EMPTY>
<!ATTLIST MUTIND
uri CDATA #REQUIRED
noType NMTOKEN #REQUIRED
id ID #REQUIRED>
<!ELEMENT MUTCONSTRUCT EMPTY>
<!ATTLIST MUTCONSTRUCT
uri CDATA #REQUIRED
noType NMTOKEN #REQUIRED
noConstr NMTOKEN #REQUIRED
id ID #REQUIRED
sort %sort; #REQUIRED>
<!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
<!ATTLIST MUTCASE
uriType CDATA #REQUIRED
noType NMTOKEN #REQUIRED
id ID #REQUIRED
sort %sort; #REQUIRED>
<!ELEMENT FIX (FixFunction+)>
<!ATTLIST FIX
noFun NMTOKEN #REQUIRED
id ID #REQUIRED
sort %sort; #REQUIRED>
<!ELEMENT COFIX (CofixFunction+)>
<!ATTLIST COFIX
noFun NMTOKEN #REQUIRED
id ID #REQUIRED
sort %sort; #REQUIRED>
<!-- Elements used in CIC terms: -->
<!ELEMENT FixFunction (type,body)>
<!ATTLIST FixFunction
name CDATA #REQUIRED
recIndex NMTOKEN #REQUIRED>
<!ELEMENT CofixFunction (type,body)>
<!ATTLIST CofixFunction
name CDATA #REQUIRED>
<!ELEMENT substitution ((%term;)?)>
<!-- Explicit named substitutions: -->
<!ELEMENT instantiate ((CONST|MUTIND|MUTCONSTRUCT),arg+)>
<!ATTLIST instantiate
id ID #IMPLIED>
<!-- Sintactic sugar for CIC terms and for CIC objects: -->
<!ELEMENT arg %term;>
<!ATTLIST arg
relUri CDATA #REQUIRED>
<!ELEMENT decl %term;>
<!ATTLIST decl
id ID #REQUIRED
type %sort; #REQUIRED
binder CDATA #IMPLIED>
<!ELEMENT def %term;>
<!ATTLIST def
id ID #REQUIRED
sort %sort; #REQUIRED
binder CDATA #IMPLIED>
<!ELEMENT target %term;>
<!ELEMENT term %term;>
<!ELEMENT type %term;>
<!ELEMENT arity %term;>
<!ELEMENT patternsType %term;>
<!ELEMENT inductiveTerm %term;>
<!ELEMENT pattern %term;>
<!ELEMENT body %term;>
|
