module Eqtrans: sig end
Justifying equality Transformers
type t = Term.t -> Term.t * Jst.jst
val id : t
id a returns (a, rho) such that rho |- a = a.
val compose : t -> t -> t
If g a = (b, rho) and f b = (c, tau) with rho |- a = b
and tau |- b = c, then compose f g a returns (c, sigma)
with sigma |- a = c.
val compose3 : t -> t -> t -> t
compose3 f g h is defined as compose f (compose g h).
val totalize : t -> t
val compose_partial1 : t -> t -> t
compose_partial1 f g a behaves like compose f g a when f
does not throw an exception. In this case, the result is g a.
val replace : Term.map -> t -> t
val apply : Term.apply -> (Term.t * Term.t) * Jst.jst -> t
val pointwise : t -> Term.t list -> Term.t list * Jst.jst
val mapargs : (Sym.t -> Term.t list -> Term.t * Jst.jst) ->
(Sym.t -> t) -> t
mapargs app f a maps f op over the arguments al of
an application a of the form op(al). If a is not
an application, Not_found is raised.
val trace : Trace.level -> string -> t -> t