package universo

  1. Overview
  2. Docs
module E = Parsers.Entry
module F = Common.Files
module L = Common.Log
module M = Api.Meta
module P = Api.Pp.Default
module R = Kernel.Rule
module T = Kernel.Term
type t = {
  1. file : F.cout F.t;
    (*

    File where universe declarations are printed

    *)
  2. meta : M.cfg;
    (*

    Meta rules that translates universes to the pre-universe variable

    *)
}
val mk_term : t -> T.term -> T.term

mk_term env t replaces all the concrete universes in t by a fresh variable using the environment env.

val mk_rule : t -> 'a R.rule -> 'a R.rule

mkrule env r replaces all the concrete universes in rule.rhs by a fresh variable using the environement env.

val mk_entry : t -> E.entry -> E.entry

mk_entry env entry replaces all the concrete universes in entry by a fresh variable using the environment env. Commands are skipped.