1 <?xml encoding="ISO-8859-1"?>
3 <!-- DTD FOR CIC OBJECTS: -->
5 <!-- CIC term declaration -->
7 <!ENTITY % term '(LAMBDA|CAST|PROD|REL|SORT|APPLY|VAR|META|IMPLICIT|CONST|
8 LETIN|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate)'>
12 <!ENTITY % sort '(Prop|Set|Type)'>
16 <!ENTITY % sequent '((Decl|Def|Hidden)*,Goal)'>
20 <!-- CSC: so far params is equal to the one of the only body. -->
21 <!ELEMENT ConstantType %term;>
22 <!ATTLIST ConstantType
24 params CDATA #REQUIRED
27 <!ELEMENT ConstantBody %term;>
28 <!ATTLIST ConstantBody
30 params CDATA #REQUIRED
33 <!ELEMENT CurrentProof (Conjecture*,body)>
34 <!ATTLIST CurrentProof
38 <!ELEMENT InductiveDefinition (InductiveType+)>
39 <!ATTLIST InductiveDefinition
40 noParams NMTOKEN #REQUIRED
41 params CDATA #REQUIRED
44 <!ELEMENT Variable (body?,type)>
49 <!ELEMENT Sequent %sequent;>
54 <!-- Elements used in CIC objects, which are not terms: -->
56 <!ELEMENT InductiveType (arity,Constructor*)>
57 <!ATTLIST InductiveType
59 inductive (true|false) #REQUIRED
62 <!ELEMENT Conjecture %sequent;>
67 <!ELEMENT Constructor %term;>
71 <!ELEMENT Decl %term;>
81 <!ELEMENT Hidden EMPTY>
85 <!ELEMENT Goal %term;>
89 <!ELEMENT LAMBDA (decl*,target)>
91 sort %sort; #REQUIRED>
93 <!ELEMENT LETIN (def*,target)>
95 sort %sort; #REQUIRED>
97 <!ELEMENT PROD (decl*,target)>
99 type %sort; #REQUIRED>
101 <!ELEMENT CAST (term,type)>
104 sort %sort; #REQUIRED>
108 value NMTOKEN #REQUIRED
109 binder CDATA #REQUIRED
111 idref IDREF #REQUIRED
112 sort %sort; #REQUIRED>
114 <!ELEMENT SORT EMPTY>
116 value CDATA #REQUIRED
119 <!ELEMENT APPLY (%term;)+>
122 sort %sort; #REQUIRED>
128 sort %sort; #REQUIRED>
130 <!-- The substitutions are ordered by increasing DeBrujin -->
131 <!-- index. An empty substitution means that that index is -->
132 <!-- not accessible. -->
133 <!ELEMENT META (substitution*)>
137 sort %sort; #REQUIRED>
139 <!ELEMENT IMPLICIT EMPTY>
143 <!ELEMENT CONST EMPTY>
147 sort %sort; #REQUIRED>
149 <!ELEMENT MUTIND EMPTY>
152 noType NMTOKEN #REQUIRED
155 <!ELEMENT MUTCONSTRUCT EMPTY>
156 <!ATTLIST MUTCONSTRUCT
158 noType NMTOKEN #REQUIRED
159 noConstr NMTOKEN #REQUIRED
161 sort %sort; #REQUIRED>
163 <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
165 uriType CDATA #REQUIRED
166 noType NMTOKEN #REQUIRED
168 sort %sort; #REQUIRED>
170 <!ELEMENT FIX (FixFunction+)>
172 noFun NMTOKEN #REQUIRED
174 sort %sort; #REQUIRED>
176 <!ELEMENT COFIX (CofixFunction+)>
178 noFun NMTOKEN #REQUIRED
180 sort %sort; #REQUIRED>
182 <!-- Elements used in CIC terms: -->
184 <!ELEMENT FixFunction (type,body)>
185 <!ATTLIST FixFunction
188 recIndex NMTOKEN #REQUIRED>
190 <!ELEMENT CofixFunction (type,body)>
191 <!ATTLIST CofixFunction
193 name CDATA #REQUIRED>
195 <!ELEMENT substitution ((%term;)?)>
197 <!-- Explicit named substitutions: -->
199 <!ELEMENT instantiate ((CONST|MUTIND|MUTCONSTRUCT),arg+)>
200 <!ATTLIST instantiate
203 <!-- Sintactic sugar for CIC terms and for CIC objects: -->
205 <!ELEMENT arg %term;>
207 relUri CDATA #REQUIRED>
209 <!ELEMENT decl %term;>
212 type %sort; #REQUIRED
213 binder CDATA #IMPLIED>
215 <!ELEMENT def %term;>
218 sort %sort; #REQUIRED
219 binder CDATA #IMPLIED>
221 <!ELEMENT target %term;>
223 <!ELEMENT term %term;>
225 <!ELEMENT type %term;>
227 <!ELEMENT arity %term;>
229 <!ELEMENT patternsType %term;>
231 <!ELEMENT inductiveTerm %term;>
233 <!ELEMENT pattern %term;>
235 <!ELEMENT body %term;>