package universo

  1. Overview
  2. Docs
module B = Kernel.Basic
module T = Kernel.Term
type univ =
  1. | Sinf
  2. | Var of B.name
  3. | Enum of int
type pred =
  1. | Axiom of univ * univ
  2. | Cumul of univ * univ
  3. | Rule of univ * univ * univ
type cstr =
  1. | Pred of pred
  2. | EqVar of B.name * B.name
module C : sig ... end
val md_theory : B.mident Stdlib.ref
val md_univ : B.mident Stdlib.ref
val pvar : unit -> B.name
val sort : unit -> B.name
val typ : unit -> B.name
val set : unit -> B.name
val prop : unit -> B.name
val univ : unit -> B.name
val cast' : unit -> B.name
val axiom : unit -> B.name
val rule : unit -> B.name
val cumul : unit -> B.name
val enum : unit -> B.name
val uzero : unit -> B.name
val usucc : unit -> B.name
val subtype : unit -> B.name
val forall : unit -> B.name
val sinf : unit -> B.name
val true_ : unit -> T.term
val term_of_level : int -> T.term
val term_of_univ : univ -> T.term
val term_of_pred : pred -> T.term
val pattern_of_level : 'a -> 'b
val is_const : B.name -> T.term -> bool
val is_var : B.mident -> T.term -> bool
val is_enum : T.term -> bool
val is_subtype : T.term -> bool
val extract_subtype : T.term -> T.term
val is_forall : T.term -> bool
val extract_forall : T.term -> T.term
val is_cast' : T.term -> bool
val extract_cast' : T.term -> T.term * T.term * T.term * T.term * T.term
val extract_level : T.term -> int
exception Not_univ
exception Not_pred
val extract_univ : T.term -> univ
val extract_pred : T.term -> pred