universo.common
Common.Constraints
universo.api
universo.checking
universo.elaboration
universo.solving
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 = {
file : F.cout F.t;
meta : M.cfg;
}
type print_cstrs = {
eqvar : (B.name * B.name) list;
axiom : (U.univ * U.univ) list;
cumul : (U.univ * U.univ) list;
rule : (U.univ * U.univ * U.univ) list;
val dummy_name : R.rule_name
val mk_rule : Kernel.Basic.name -> Kernel.Basic.name -> 'a R.rule
val print_rule : (Format.formatter -> 'a -> unit) -> Format.formatter -> ('a * 'a) -> unit
val print_eq_var : Format.formatter -> (Kernel.Basic.name * Kernel.Basic.name) -> unit
val print_predicate : 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.
mk_var_cstre env f l r
l =?= r
val deps : B.mident list ref
val mk_cstr : t -> (B.name -> B.name -> 'a) -> U.cstr -> bool
val get_deps : unit -> B.mident list
val flush : unit -> unit