package logtk

  1. Overview
  2. Docs

Module Subst.Projection

type t = private {
  1. scope : Scoped.scope;
  2. subst : subst;
  3. 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