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)>
47 params CDATA #REQUIRED
50 <!ELEMENT Sequent %sequent;>
55 <!-- Elements used in CIC objects, which are not terms: -->
57 <!ELEMENT InductiveType (arity,Constructor*)>
58 <!ATTLIST InductiveType
60 inductive (true|false) #REQUIRED
63 <!ELEMENT Conjecture %sequent;>
68 <!ELEMENT Constructor %term;>
72 <!ELEMENT Decl %term;>
82 <!ELEMENT Hidden EMPTY>
86 <!ELEMENT Goal %term;>
90 <!ELEMENT LAMBDA (decl*,target)>
92 sort %sort; #REQUIRED>
94 <!ELEMENT LETIN (def*,target)>
96 sort %sort; #REQUIRED>
98 <!ELEMENT PROD (decl*,target)>
100 type %sort; #REQUIRED>
102 <!ELEMENT CAST (term,type)>
105 sort %sort; #REQUIRED>
109 value NMTOKEN #REQUIRED
110 binder CDATA #REQUIRED
112 idref IDREF #REQUIRED
113 sort %sort; #REQUIRED>
115 <!ELEMENT SORT EMPTY>
117 value CDATA #REQUIRED
120 <!ELEMENT APPLY (%term;)+>
123 sort %sort; #REQUIRED>
129 sort %sort; #REQUIRED>
131 <!-- The substitutions are ordered by increasing DeBrujin -->
132 <!-- index. An empty substitution means that that index is -->
133 <!-- not accessible. -->
134 <!ELEMENT META (substitution*)>
138 sort %sort; #REQUIRED>
140 <!ELEMENT IMPLICIT EMPTY>
144 <!ELEMENT CONST EMPTY>
148 sort %sort; #REQUIRED>
150 <!ELEMENT MUTIND EMPTY>
153 noType NMTOKEN #REQUIRED
156 <!ELEMENT MUTCONSTRUCT EMPTY>
157 <!ATTLIST MUTCONSTRUCT
159 noType NMTOKEN #REQUIRED
160 noConstr NMTOKEN #REQUIRED
162 sort %sort; #REQUIRED>
164 <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
166 uriType CDATA #REQUIRED
167 noType NMTOKEN #REQUIRED
169 sort %sort; #REQUIRED>
171 <!ELEMENT FIX (FixFunction+)>
173 noFun NMTOKEN #REQUIRED
175 sort %sort; #REQUIRED>
177 <!ELEMENT COFIX (CofixFunction+)>
179 noFun NMTOKEN #REQUIRED
181 sort %sort; #REQUIRED>
183 <!-- Elements used in CIC terms: -->
185 <!ELEMENT FixFunction (type,body)>
186 <!ATTLIST FixFunction
189 recIndex NMTOKEN #REQUIRED>
191 <!ELEMENT CofixFunction (type,body)>
192 <!ATTLIST CofixFunction
194 name CDATA #REQUIRED>
196 <!ELEMENT substitution ((%term;)?)>
198 <!-- Explicit named substitutions: -->
200 <!ELEMENT instantiate ((CONST|MUTIND|MUTCONSTRUCT|VAR),arg+)>
201 <!ATTLIST instantiate
204 <!-- Sintactic sugar for CIC terms and for CIC objects: -->
206 <!ELEMENT arg %term;>
208 relUri CDATA #REQUIRED>
210 <!ELEMENT decl %term;>
213 type %sort; #REQUIRED
214 binder CDATA #IMPLIED>
216 <!ELEMENT def %term;>
219 sort %sort; #REQUIRED
220 binder CDATA #IMPLIED>
222 <!ELEMENT target %term;>
224 <!ELEMENT term %term;>
226 <!ELEMENT type %term;>
228 <!ELEMENT arity %term;>
230 <!ELEMENT patternsType %term;>
232 <!ELEMENT inductiveTerm %term;>
234 <!ELEMENT pattern %term;>
236 <!ELEMENT body %term;>