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