package universo

  1. Overview
  2. Docs
package universo
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Common.UniversesSource

Sourcetype univ =
  1. | Sinf
  2. | Var of B.name
  3. | Enum of int
Sourcetype pred =
  1. | Axiom of univ * univ
  2. | Cumul of univ * univ
  3. | Rule of univ * univ * univ
Sourcetype cstr =
  1. | Pred of pred
  2. | EqVar of B.name * B.name
Sourcemodule C : sig ... end
Sourceval md_theory : B.mident ref
Sourceval md_univ : B.mident ref
Sourceval pvar : unit -> B.name
Sourceval sort : unit -> B.name
Sourceval typ : unit -> B.name
Sourceval set : unit -> B.name
Sourceval prop : unit -> B.name
Sourceval univ : unit -> B.name
Sourceval cast' : unit -> B.name
Sourceval axiom : unit -> B.name
Sourceval rule : unit -> B.name
Sourceval cumul : unit -> B.name
Sourceval enum : unit -> B.name
Sourceval uzero : unit -> B.name
Sourceval usucc : unit -> B.name
Sourceval subtype : unit -> B.name
Sourceval forall : unit -> B.name
Sourceval sinf : unit -> B.name
Sourceval true_ : unit -> T.term
Sourceval term_of_level : int -> T.term
Sourceval term_of_univ : univ -> T.term
Sourceval term_of_pred : pred -> T.term
Sourceval pattern_of_level : 'a -> 'b
Sourceval is_const : B.name -> T.term -> bool
Sourceval is_var : B.mident -> T.term -> bool
Sourceval is_enum : T.term -> bool
Sourceval is_subtype : T.term -> bool
Sourceval extract_subtype : T.term -> T.term
Sourceval is_forall : T.term -> bool
Sourceval extract_forall : T.term -> T.term
Sourceval is_cast' : T.term -> bool
Sourceval extract_cast' : T.term -> T.term * T.term * T.term * T.term * T.term
Sourceval extract_level : T.term -> int
Sourceexception Not_univ
Sourceexception Not_pred
Sourceval extract_univ : T.term -> univ
Sourceval 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