Module Logtk__Subst.Projection

type t = private {
scope : Logtk.Scoped.scope;
subst : subst;
renaming : Renaming.t;
}

A representation of the substitution for a given scope, after applying the renaming.

val subst : t -> subst
val scope : t -> Logtk.Scoped.scope
val renaming : t -> Renaming.t
val bindings : t -> (var * term) list

List of bindings of the projection. Variables in the domain are bound in scope subst, but variables in terms of the codomain are bound in the renaming

val as_inst : ?⁠allow_free_db:bool -> ctx:Logtk.Term.Conv.ctx -> t -> Logtk.Type.t Logtk.HVar.t list -> (Logtk.TypedSTerm.t, Logtk.TypedSTerm.t) Logtk.Var.Subst.t

Convert into an instantiation on the given variables

val is_empty : t -> bool
val make : Renaming.t -> subst Logtk.Scoped.t -> t
val pp : t CCFormat.printer