package logtk

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type term = LogtkHOTerm.t
type t = subst
val mem : t -> term -> scope -> bool

Variable is bound?

val apply : t -> renaming:Renaming.t -> term -> scope -> term

Apply the substitution to the given term/type.

  • parameter renaming

    used to desambiguate free variables from distinct scopes

val apply_no_renaming : t -> term -> scope -> term

Same as apply, but performs no renaming of free variables. Caution, can entail collisions between scopes!

val bind : t -> term -> scope -> term -> scope -> t

Add v -> t to the substitution. Both terms have a context.

  • raises Invalid_argument

    if v is already bound in the same context, to another term.