1 <?xml encoding="ISO-8859-1"?>
3 <!-- Copyright (C) 2000, HELM Team -->
5 <!-- This file is part of HELM, an Hypertextual, Electronic -->
6 <!-- Library of Mathematics, developed at the Computer Science -->
7 <!-- Department, University of Bologna, Italy. -->
9 <!-- HELM is free software; you can redistribute it and/or -->
10 <!-- modify it under the terms of the GNU General Public License -->
11 <!-- as published by the Free Software Foundation; either version 2 -->
12 <!-- of the License, or (at your option) any later version. -->
14 <!-- HELM is distributed in the hope that it will be useful, -->
15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of -->
16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -->
17 <!-- GNU General Public License for more details. -->
19 <!-- You should have received a copy of the GNU General Public License -->
20 <!-- along with HELM; if not, write to the Free Software -->
21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, -->
22 <!-- MA 02111-1307, USA. -->
24 <!-- For details, see the HELM World-Wide-Web page, -->
25 <!-- http://cs.unibo.it/helm/. -->
27 <!--*****************************************************************-->
28 <!-- DTD FOR CIC OBJECTS: -->
29 <!-- First draft: September 1999, Claudio Sacerdoti Coen -->
30 <!-- Revised: February 3 2000, Claudio Sacerdoti Coen, Irene Schena -->
31 <!-- Last Revision: April 4 2000, Claudio Sacerdoti Coen -->
32 <!-- Last Revision: June 19 2000, Claudio Sacerdoti Coen -->
33 <!-- Last Revision: June 20 2000, Claudio Sacerdoti Coen -->
34 <!--*****************************************************************-->
36 <!-- CIC term declaration -->
38 <!ENTITY % term '(LAMBDA|CAST|PROD|REL|SORT|APPLY|VAR|META|IMPLICIT|CONST|
39 LETIN|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX)'>
43 <!ENTITY % sort '(Prop|Set|Type)'>
47 <!ENTITY % sequent '((Decl|Def|Hidden)*,Goal)'>
51 <!ELEMENT Definition (body, type)>
54 params CDATA #REQUIRED
55 paramMode (POSSIBLE) #IMPLIED
58 <!ELEMENT Axiom (type)>
61 params CDATA #REQUIRED
64 <!ELEMENT CurrentProof (Conjecture*,body,type)>
65 <!ATTLIST CurrentProof
69 <!ELEMENT InductiveDefinition (InductiveType+)>
70 <!ATTLIST InductiveDefinition
71 noParams NMTOKEN #REQUIRED
72 params CDATA #REQUIRED
75 <!ELEMENT Variable (body?,type)>
80 <!ELEMENT Sequent %sequent;>
85 <!-- Elements used in CIC objects, which are not terms: -->
87 <!ELEMENT InductiveType (arity,Constructor*)>
88 <!ATTLIST InductiveType
90 inductive (true|false) #REQUIRED>
92 <!ELEMENT Conjecture %sequent;>
97 <!ELEMENT Constructor %term;>
101 <!ELEMENT Decl %term;>
106 <!ELEMENT Def %term;>
111 <!ELEMENT Hidden EMPTY>
115 <!ELEMENT Goal %term;>
119 <!ELEMENT LAMBDA (source,target)>
122 sort %sort; #REQUIRED>
124 <!ELEMENT LETIN (term,letintarget)>
127 sort %sort; #REQUIRED>
129 <!ELEMENT PROD (source,target)>
132 type %sort; #REQUIRED>
134 <!ELEMENT CAST (term,type)>
137 sort %sort; #REQUIRED>
141 value NMTOKEN #REQUIRED
142 binder CDATA #REQUIRED
144 sort %sort; #REQUIRED>
146 <!ELEMENT SORT EMPTY>
148 value CDATA #REQUIRED
151 <!ELEMENT APPLY (%term;)+>
154 sort %sort; #REQUIRED>
158 relUri CDATA #REQUIRED
160 sort %sort; #REQUIRED>
162 <!-- The substitutions are ordered by increasing DeBrujin -->
163 <!-- index. An empty substitution means that that index is -->
164 <!-- not accessible. -->
165 <!ELEMENT META (substitution*)>
169 sort %sort; #REQUIRED>
171 <!ELEMENT IMPLICIT EMPTY>
175 <!ELEMENT CONST EMPTY>
179 sort %sort; #REQUIRED>
181 <!ELEMENT MUTIND EMPTY>
184 noType NMTOKEN #REQUIRED
187 <!ELEMENT MUTCONSTRUCT EMPTY>
188 <!ATTLIST MUTCONSTRUCT
190 noType NMTOKEN #REQUIRED
191 noConstr NMTOKEN #REQUIRED
193 sort %sort; #REQUIRED>
195 <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
197 uriType CDATA #REQUIRED
198 noType NMTOKEN #REQUIRED
200 sort %sort; #REQUIRED>
202 <!ELEMENT FIX (FixFunction+)>
204 noFun NMTOKEN #REQUIRED
206 sort %sort; #REQUIRED>
208 <!ELEMENT COFIX (CofixFunction+)>
210 noFun NMTOKEN #REQUIRED
212 sort %sort; #REQUIRED>
214 <!-- Elements used in CIC terms: -->
216 <!ELEMENT FixFunction (type,body)>
217 <!ATTLIST FixFunction
219 recIndex NMTOKEN #REQUIRED>
221 <!ELEMENT CofixFunction (type,body)>
222 <!ATTLIST CofixFunction
223 name CDATA #REQUIRED>
225 <!ELEMENT substitution ((%term;)?)>
227 <!-- Sintactic sugar for CIC terms and for CIC objects: -->
229 <!ELEMENT source %term;>
231 <!ELEMENT target %term;>
233 binder CDATA #IMPLIED>
235 <!ELEMENT letintarget %term;>
236 <!ATTLIST letintarget
237 binder CDATA #REQUIRED>
239 <!ELEMENT term %term;>
241 <!ELEMENT type %term;>
243 <!ELEMENT arity %term;>
245 <!ELEMENT patternsType %term;>
247 <!ELEMENT inductiveTerm %term;>
249 <!ELEMENT pattern %term;>
251 <!ELEMENT body %term;>