package universo

You can search for identifiers within the package.

in-package search v0.2.0

A tool for Dedukti to play with universes

Install

sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c

sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c

module E = Parsers.Entry

Sourcemodule F = Common.Files

Sourcemodule L = Common.Log

Sourcemodule M = Api.Meta

Sourcemodule P = Api.Pp.Default

module R = Kernel.Rule

module T = Kernel.Term

Sourcetype 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
*)

}

Sourceval 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.

Sourceval 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.

Sourceval 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.