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)'>
48 <!ELEMENT Definition (body, type)>
51 params CDATA #REQUIRED
52 paramMode (POSSIBLE) #IMPLIED
55 <!ELEMENT Axiom (type)>
58 params CDATA #REQUIRED
61 <!ELEMENT CurrentProof (Conjecture*,body,type)>
62 <!ATTLIST CurrentProof
66 <!ELEMENT InductiveDefinition (InductiveType+)>
67 <!ATTLIST InductiveDefinition
68 noParams NMTOKEN #REQUIRED
69 params CDATA #REQUIRED
72 <!ELEMENT Variable (body?,type)>
77 <!-- Elements used in CIC objects, which are not terms: -->
79 <!ELEMENT InductiveType (arity,Constructor*)>
80 <!ATTLIST InductiveType
82 inductive (true|false) #REQUIRED>
84 <!ELEMENT Conjecture %term;>
88 <!ELEMENT Constructor %term;>
94 <!ELEMENT LAMBDA (source,target)>
97 sort %sort; #REQUIRED>
99 <!ELEMENT LETIN (term,letintarget)>
102 sort %sort; #REQUIRED>
104 <!ELEMENT PROD (source,target)>
107 type %sort; #REQUIRED>
109 <!ELEMENT CAST (term,type)>
112 sort %sort; #REQUIRED>
116 value NMTOKEN #REQUIRED
117 binder CDATA #REQUIRED
119 sort %sort; #REQUIRED>
121 <!ELEMENT SORT EMPTY>
123 value CDATA #REQUIRED
126 <!ELEMENT APPLY (%term;)+>
129 sort %sort; #REQUIRED>
133 relUri CDATA #REQUIRED
135 sort %sort; #REQUIRED>
137 <!ELEMENT META EMPTY>
141 sort %sort; #REQUIRED>
143 <!ELEMENT IMPLICIT EMPTY>
147 <!ELEMENT CONST EMPTY>
151 sort %sort; #REQUIRED>
153 <!ELEMENT MUTIND EMPTY>
156 noType NMTOKEN #REQUIRED
159 <!ELEMENT MUTCONSTRUCT EMPTY>
160 <!ATTLIST MUTCONSTRUCT
162 noType NMTOKEN #REQUIRED
163 noConstr NMTOKEN #REQUIRED
165 sort %sort; #REQUIRED>
167 <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
169 uriType CDATA #REQUIRED
170 noType NMTOKEN #REQUIRED
172 sort %sort; #REQUIRED>
174 <!ELEMENT FIX (FixFunction+)>
176 noFun NMTOKEN #REQUIRED
178 sort %sort; #REQUIRED>
180 <!ELEMENT COFIX (CofixFunction+)>
182 noFun NMTOKEN #REQUIRED
184 sort %sort; #REQUIRED>
186 <!-- Elements used in CIC terms: -->
188 <!ELEMENT FixFunction (type,body)>
189 <!ATTLIST FixFunction
191 recIndex NMTOKEN #REQUIRED>
193 <!ELEMENT CofixFunction (type,body)>
194 <!ATTLIST CofixFunction
195 name CDATA #REQUIRED>
197 <!-- Sintactic sugar for CIC terms and for CIC objects: -->
199 <!ELEMENT source %term;>
201 <!ELEMENT target %term;>
203 binder CDATA #IMPLIED>
205 <!ELEMENT letintarget %term;>
206 <!ATTLIST letintarget
207 binder CDATA #REQUIRED>
209 <!ELEMENT term %term;>
211 <!ELEMENT type %term;>
213 <!ELEMENT arity %term;>
215 <!ELEMENT patternsType %term;>
217 <!ELEMENT inductiveTerm %term;>
219 <!ELEMENT pattern %term;>
221 <!ELEMENT body %term;>