package universo

  1. Overview
  2. Docs
module B = Kernel.Basic
module F = Files
module R = Kernel.Rule
module S = Kernel.Signature
module T = Kernel.Term
module U = Universes
module M = Api.Meta
type t = {
  1. file : F.cout F.t;
  2. meta : M.cfg;
}
type print_cstrs = {
  1. eqvar : (B.name * B.name) list;
  2. axiom : (U.univ * U.univ) list;
  3. cumul : (U.univ * U.univ) list;
  4. rule : (U.univ * U.univ * U.univ) list;
}
val dummy_name : R.rule_name
val print_rule : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> ('b * 'c) -> unit
val print_eq_var : Stdlib.Format.formatter -> (Kernel.Basic.name * Kernel.Basic.name) -> unit
val print_predicate : Stdlib.Format.formatter -> U.pred -> unit
val mk_var_cstr : (B.name -> B.name -> 'a) -> B.name -> B.name -> B.name * B.name

mk_var_cstre env f l r add the constraint l =?= r. Call f on l and r such that l >= r.

val deps : B.mident list Stdlib.ref
val mk_cstr : t -> (B.name -> B.name -> 'a) -> U.cstr -> bool
val get_deps : unit -> B.mident list
val flush : unit -> unit