]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/cic/helmLibraryObjects.mli
more comments
[helm.git] / helm / software / components / cic / helmLibraryObjects.mli
1 (* Copyright (C) 2004, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 module Logic :
27   sig
28     val absurd_URI :    UriManager.uri
29     val and_ind_URI :   UriManager.uri
30     val and_URI :       UriManager.uri
31     val eq_ind_r_URI :  UriManager.uri
32     val eq_ind_URI :    UriManager.uri
33     val eq_URI :        UriManager.uri
34     val ex_ind_URI :    UriManager.uri
35     val ex_URI :        UriManager.uri
36     val false_ind_URI : UriManager.uri
37     val false_URI :     UriManager.uri
38     val iff_URI :       UriManager.uri
39     val not_URI :       UriManager.uri
40     val or_URI :        UriManager.uri
41     val sym_eq_URI :    UriManager.uri
42     val trans_eq_URI :  UriManager.uri
43     val true_URI :      UriManager.uri
44
45     val and_SURI :      string
46     val eq_SURI :       string
47     val ex_SURI :       string
48     val iff_SURI :      string
49     val not_SURI :      string
50     val or_SURI :       string
51
52     val and_XURI :      string
53     val eq_XURI :       string
54     val ex_XURI :       string
55     val or_XURI :       string
56   end
57
58 module Datatypes :
59   sig
60     val bool_URI :      UriManager.uri
61     val nat_URI :       UriManager.uri
62
63     val trueb :         Cic.term
64     val falseb :        Cic.term
65     val zero :          Cic.term
66     val succ :          Cic.term
67   end
68
69 module Reals :
70   sig
71     val pow_URI :       UriManager.uri
72     val r0_URI :        UriManager.uri
73     val r1_URI :        UriManager.uri
74     val rdiv_URI :      UriManager.uri
75     val rge_URI :       UriManager.uri
76     val rgt_URI :       UriManager.uri
77     val rinv_r1_URI :   UriManager.uri
78     val rinv_URI :      UriManager.uri
79     val rle_URI :       UriManager.uri
80     val rlt_URI :       UriManager.uri
81     val rminus_URI :    UriManager.uri
82     val rmult_URI :     UriManager.uri
83     val ropp_URI :      UriManager.uri
84     val rplus_URI :     UriManager.uri
85     val rtheory_URI :   UriManager.uri
86     val r_URI :         UriManager.uri
87
88     val r0_SURI :       string
89     val r1_SURI :       string
90     val rdiv_SURI :     string
91     val rge_SURI :      string
92     val rgt_SURI :      string
93     val rinv_SURI :     string
94     val rle_SURI :      string
95     val rlt_SURI :      string
96     val rminus_SURI :   string
97     val rmult_SURI :    string
98     val ropp_SURI :     string
99     val rplus_SURI :    string
100
101     val r0 :            Cic.term
102     val r1 :            Cic.term
103     val r :             Cic.term
104     val rmult :         Cic.term
105     val ropp :          Cic.term
106     val rplus :         Cic.term
107     val rtheory :       Cic.term
108   end
109
110 module Peano :
111   sig
112     val ge_URI :        UriManager.uri
113     val gt_URI :        UriManager.uri
114     val le_URI :        UriManager.uri
115     val lt_URI :        UriManager.uri
116     val minus_URI :     UriManager.uri
117     val mult_URI :      UriManager.uri
118     val plus_URI :      UriManager.uri
119     val pred_URI :      UriManager.uri
120
121     val ge_SURI :       string
122     val gt_SURI :       string
123     val le_SURI :       string
124     val lt_SURI :       string
125     val minus_SURI :    string
126     val mult_SURI :     string
127     val plus_SURI :     string
128
129     val le_XURI :       string
130
131     val mult :          Cic.term
132     val plus :          Cic.term
133     val pred :          Cic.term
134   end
135
136 module BinPos :
137   sig
138     val pminus_URI :    UriManager.uri
139     val pmult_URI :     UriManager.uri
140     val positive_URI :  UriManager.uri
141     val pplus_URI :     UriManager.uri
142
143     val pminus_SURI :   string
144     val pmult_SURI :    string
145     val positive_SURI : string
146     val pplus_SURI :    string
147
148     val pminus :        Cic.term
149     val pmult :         Cic.term
150     val pplus :         Cic.term
151     val xH :            Cic.term
152     val xI :            Cic.term
153     val xO :            Cic.term
154   end
155
156 module BinInt :
157   sig
158     val zminus_URI :    UriManager.uri
159     val zmult_URI :     UriManager.uri
160     val zopp_URI :      UriManager.uri
161     val zplus_URI :     UriManager.uri
162     val zpower_URI :    UriManager.uri
163     val z_URI :         UriManager.uri
164
165     val zminus_SURI :   string
166     val zopp_SURI :     string
167     val zplus_SURI :    string
168     val z_SURI :        string
169
170     val z0 :            Cic.term
171     val zminus :        Cic.term
172     val zmult :         Cic.term
173     val zneg :          Cic.term
174     val zopp :          Cic.term
175     val zplus :         Cic.term
176     val zpos :          Cic.term
177   end
178
179 val build_bin_pos : int -> Cic.term
180 val build_nat :     int -> Cic.term
181 val build_real :    int -> Cic.term
182