package universo

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

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 = {

file : F.cout F.t;
(*
File where universe declarations are printed
*)
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.