Module Subst.Projection

type t = private {
scope : 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 -> 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:Term.Conv.ctx -> t -> Type.t HVar.t list -> (TypedSTerm.t, TypedSTerm.t) Var.Subst.t

Convert into an instantiation on the given variables

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