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
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
|
<?xml encoding="ISO-8859-1"?>
<!-- Copyright (C) 2000-2004, HELM Team -->
<!-- -->
<!-- This file is part of HELM, an Hypertextual, Electronic -->
<!-- Library of Mathematics, developed at the Computer Science -->
<!-- Department, University of Bologna, Italy. -->
<!-- -->
<!-- HELM is free software; you can redistribute it and/or -->
<!-- modify it under the terms of the GNU General Public License -->
<!-- as published by the Free Software Foundation; either version 2 -->
<!-- of the License, or (at your option) any later version. -->
<!-- -->
<!-- HELM is distributed in the hope that it will be useful, -->
<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of -->
<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -->
<!-- GNU General Public License for more details. -->
<!-- -->
<!-- You should have received a copy of the GNU General Public License -->
<!-- along with HELM; if not, write to the Free Software -->
<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, -->
<!-- MA 02111-1307, USA. -->
<!-- -->
<!-- For details, see the HELM World-Wide-Web page, -->
<!-- http://cs.unibo.it/helm/. -->
<!-- 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|CProp)'>
<!-- CIC sequents -->
<!ENTITY % sequent '((Decl|Def|Hidden)*,Goal)'>
<!-- CIC objects: -->
<!ELEMENT ConstantType %term;>
<!ATTLIST ConstantType
name CDATA #REQUIRED
params 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
params 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
id ID #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
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
uri 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
id ID #REQUIRED
recIndex NMTOKEN #REQUIRED>
<!ELEMENT CofixFunction (type,body)>
<!ATTLIST CofixFunction
id ID #REQUIRED
name CDATA #REQUIRED>
<!ELEMENT substitution ((%term;)?)>
<!-- Explicit named substitutions: -->
<!ELEMENT instantiate ((CONST|MUTIND|MUTCONSTRUCT|VAR),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;>
|
