1 <?xml encoding="ISO-8859-1"?>
3 <!--*****************************************************************-->
4 <!-- DTD FOR CIC OBJECTS: -->
5 <!-- First draft: September 1999, Claudio Sacerdoti Coen -->
6 <!-- Revised: February 3 2000, Claudio Sacerdoti Coen, Irene Schena -->
7 <!-- Last Revision: April 4 2000, Claudio Sacerdoti Coen -->
8 <!-- Last Revision: June 19 2000, Claudio Sacerdoti Coen -->
9 <!-- Last Revision: June 20 2000, Claudio Sacerdoti Coen -->
10 <!--*****************************************************************-->
12 <!-- CIC term declaration -->
14 <!ENTITY % term '(LAMBDA|CAST|PROD|REL|SORT|APPLY|VAR|META|IMPLICIT|CONST|
15 ABST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX)'>
19 <!ELEMENT Definition (body, type)>
22 params CDATA #REQUIRED
23 paramMode (POSSIBLE) #IMPLIED
26 <!ELEMENT Axiom (type)>
29 params CDATA #REQUIRED
32 <!ELEMENT CurrentProof (Conjecture*,body,type)>
33 <!ATTLIST CurrentProof
37 <!ELEMENT InductiveDefinition (InductiveType+)>
38 <!ATTLIST InductiveDefinition
39 noParams NMTOKEN #REQUIRED
40 params CDATA #REQUIRED
43 <!ELEMENT Variable (type)>
48 <!-- Elements used in CIC objects, which are not terms: -->
50 <!ELEMENT InductiveType (arity,Constructor*)>
51 <!ATTLIST InductiveType
53 inductive (true|false) #REQUIRED>
55 <!ELEMENT Conjecture %term;>
59 <!ELEMENT Constructor %term;>
65 <!ELEMENT LAMBDA (source,target)>
69 <!ELEMENT PROD (source,target)>
73 <!ELEMENT CAST (term,type)>
79 value NMTOKEN #REQUIRED
80 binder CDATA #REQUIRED
88 <!ELEMENT APPLY (%term;)+>
94 relUri CDATA #REQUIRED
102 <!ELEMENT IMPLICIT EMPTY>
106 <!ELEMENT CONST EMPTY>
111 <!ELEMENT ABST EMPTY>
116 <!ELEMENT MUTIND EMPTY>
119 noType NMTOKEN #REQUIRED
122 <!ELEMENT MUTCONSTRUCT EMPTY>
123 <!ATTLIST MUTCONSTRUCT
125 noType NMTOKEN #REQUIRED
126 noConstr NMTOKEN #REQUIRED
129 <!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
131 uriType CDATA #REQUIRED
132 noType NMTOKEN #REQUIRED
135 <!ELEMENT FIX (FixFunction+)>
137 noFun NMTOKEN #REQUIRED
140 <!ELEMENT COFIX (CofixFunction+)>
142 noFun NMTOKEN #REQUIRED
145 <!-- Elements used in CIC terms: -->
147 <!ELEMENT FixFunction (type,body)>
148 <!ATTLIST FixFunction
150 recIndex NMTOKEN #REQUIRED>
152 <!ELEMENT CofixFunction (type,body)>
153 <!ATTLIST CofixFunction
154 name CDATA #REQUIRED>
156 <!-- Sintactic sugar for CIC terms and for CIC objects: -->
158 <!ELEMENT source %term;>
160 <!ELEMENT target %term;>
162 binder CDATA #IMPLIED>
164 <!ELEMENT term %term;>
166 <!ELEMENT type %term;>
168 <!ELEMENT arity %term;>
170 <!ELEMENT patternsType %term;>
172 <!ELEMENT inductiveTerm %term;>
174 <!ELEMENT pattern %term;>
176 <!ELEMENT body %term;>