package universo

  1. Overview
  2. Docs
module M = Api.Meta
module T = Kernel.Term
module U = Universes
type theory = (U.pred * bool) list
type theory_maker = int -> theory
val enumerate : int -> U.univ list
val is_true : M.cfg -> U.pred -> bool

is_true meta p check if the predicate p is true in the original theory.

val is_true_axiom : M.cfg -> U.univ -> U.univ -> U.pred * bool

is_true_axiom meta s s' check if the predicate Axiom s s' is true in the original theory.

val is_true_cumul : M.cfg -> U.univ -> U.univ -> U.pred * bool

is_true_cumul meta s s' check if the predicate Cumul s s' is true in the original theory.

val is_true_rule : M.cfg -> U.univ -> U.univ -> U.univ -> U.pred * bool

is_true_rule meta s s' s'' check if the predicate Rule s s' s'' is true in the original theory.

module Util : sig ... end
val mk_theory : M.cfg -> int -> theory

mk_theory meta i computes a theory for the universes up to i. A theory is an array for each predicate that tells if the predicate holds. The array is index by universes and its dimension is the arity of the predicate.