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 ref
val md_univ : B.mident 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct