]> matita.cs.unibo.it Git - helm.git/blob - helm/dtd/cicobject.dtd
commented Record type constructor
[helm.git] / helm / dtd / cicobject.dtd
1 <?xml encoding="ISO-8859-1"?>
2
3 <!-- Copyright (C) 2000, HELM Team                                     -->
4 <!--                                                                   -->
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.                         -->
8 <!--                                                                   -->
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.            -->
13 <!--                                                                   -->
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.                      -->
18 <!--                                                                   -->
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.                                              -->
23 <!--                                                                   -->
24 <!-- For details, see the HELM World-Wide-Web page,                    -->
25 <!-- http://cs.unibo.it/helm/.                                         -->
26
27 <!--*****************************************************************-->
28 <!-- DTD FOR CIC OBJECTS AT LEVEL OF MATHML CONTENT:                 -->
29 <!--  First draft: March 21, Claudio Sacerdoti Coen, Irene Schena    -->
30 <!--*****************************************************************-->
31
32 <!ENTITY % mathml SYSTEM "mathml2.dtd">
33
34 %mathml;
35
36 <!ENTITY % term '(annotation|%math.qname;)'>
37
38 <!-- Terms: -->
39
40 <!ELEMENT annotation (#PCDATA|annotation|%math.qname;)*>
41 <!ATTLIST annotation
42           xmlns:m    CDATA #REQUIRED>
43
44 <!-- CIC objects: -->
45
46 <!ELEMENT Definition (Params,body,type)>
47 <!ATTLIST Definition
48           name       CDATA      #REQUIRED
49           xmlns:m    CDATA      #REQUIRED>
50
51 <!ELEMENT Axiom (Params,type)>
52 <!ATTLIST Axiom
53           name   CDATA #REQUIRED
54           xmlns:m    CDATA      #REQUIRED>
55
56 <!ELEMENT CurrentProof (Conjecture*,body,type)>
57 <!ATTLIST CurrentProof
58           name CDATA #REQUIRED
59           xmlns:m    CDATA      #REQUIRED>
60
61 <!ELEMENT InductiveDefinition (Params,Param*,InductiveType+)>
62 <!ATTLIST InductiveDefinition
63           xmlns:m    CDATA      #REQUIRED>
64
65 <!ELEMENT Variable (body?,type)>
66 <!ATTLIST Variable
67           name CDATA #REQUIRED
68           xmlns:m    CDATA      #REQUIRED>
69
70 <!ELEMENT Sequent ((Decl|Def)*,Goal)>
71 <!ATTLIST Sequent
72           id   ID    #REQUIRED>
73
74 <!-- Elements used in CIC objects, which are not terms: -->
75
76 <!ELEMENT InductiveType (arity,Constructor*)>
77 <!ATTLIST InductiveType
78           name      CDATA        #REQUIRED
79           inductive (true|false) #REQUIRED>
80
81 <!ELEMENT Conjecture %term;>
82 <!ATTLIST Conjecture
83           no NMTOKEN #REQUIRED>
84
85 <!ELEMENT Constructor %term;>
86 <!ATTLIST Constructor
87           name CDATA #REQUIRED>
88
89 <!ELEMENT Param %term;>
90 <!ATTLIST Param
91           name CDATA #REQUIRED>
92
93 <!ELEMENT Params (param)*>
94
95 <!ELEMENT param %term;>
96
97 <!ELEMENT Decl %term;>
98 <!ATTLIST Decl
99           name CDATA #REQUIRED>
100
101 <!ELEMENT Def %term;>
102 <!ATTLIST Def
103           name CDATA #REQUIRED>
104
105 <!ELEMENT Goal %term;>
106
107 <!-- Sintactic sugar for CIC objects: -->
108
109 <!ELEMENT type  %term;>
110
111 <!ELEMENT arity %term;>
112
113 <!ELEMENT body  %term;>
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137