class HasSubstitution (α : Type u) (β : Type v) : Type (max u v)

Typeclass for substitution relations and access to their notation.

• subst (t : α) (x : β) (t' : α) : α

  Substitution function. Replaces x in t with t'.

def «term_[_:=_]» : Lean.TrailingParserDescr

Notation for substitution.

Equations

• One or more equations did not get rendered due to their size.