helm/ocaml/cic/helmLibraryObjects.ml

   1
   2 let uri = UriManager.uri_of_string
   3
   4 let const ?(subst = []) uri = Cic.Const (uri, subst)
   5 let var ?(subst = []) uri = Cic.Var (uri, subst)
   6 let mutconstruct ?(subst = []) uri typeno consno =
   7   Cic.MutConstruct (uri, typeno, consno, subst)
   8
   9 module Logic =
  10   struct
  11     let eq_URI = uri "cic:/Coq/Init/Logic/eq.ind"
  12     let true_URI = uri "cic:/Coq/Init/Logic/True.ind"
  13     let false_URI = uri "cic:/Coq/Init/Logic/False.ind"
  14   end
  15
  16 module Logic_Type =
  17   struct
  18     let eqt_URI = uri "cic:/Coq/Init/Logic_Type/eqT.ind"
  19     let sym_eqt_URI = uri "cic:/Coq/Init/Logic_Type/sym_eqT.con"
  20
  21     let refl_eqt = mutconstruct eqt_URI 0 1
  22     let sym_eqt = const sym_eqt_URI
  23   end
  24
  25 module Datatypes =
  26   struct
  27     let bool_URI = uri "cic:/Coq/Init/Datatypes/bool.ind"
  28     let nat_URI = uri "cic:/Coq/Init/Datatypes/nat.ind"
  29
  30     let trueb = mutconstruct bool_URI 0 1
  31     let falseb = mutconstruct bool_URI 0 2
  32     let zero = mutconstruct nat_URI 0 1
  33     let succ = mutconstruct nat_URI 0 2
  34   end
  35
  36 module Reals =
  37   struct
  38     let r_URI = uri "cic:/Coq/Reals/Rdefinitions/R.con"
  39     let rplus_URI = uri "cic:/Coq/Reals/Rdefinitions/Rplus.con"
  40     let rmult_URI = uri "cic:/Coq/Reals/Rdefinitions/Rmult.con"
  41     let ropp_URI = uri "cic:/Coq/Reals/Rdefinitions/Ropp.con"
  42     let r0_URI = uri "cic:/Coq/Reals/Rdefinitions/R0.con"
  43     let r1_URI = uri "cic:/Coq/Reals/Rdefinitions/R1.con"
  44     let rtheory_URI = uri "cic:/Coq/Reals/Rbase/RTheory.con"
  45
  46     let r = const r_URI
  47     let rplus = const rplus_URI
  48     let rmult = const rmult_URI
  49     let ropp = const ropp_URI
  50     let r0 = const r0_URI
  51     let r1 = const r1_URI
  52     let rtheory = const rtheory_URI
  53   end
  54