Notation typeclass for substitution.

class Cslib.HasSubstitution (α : Type u) (β : Type v) (γ : Type w) : Type (max (max u v) w)

Typeclass for substitution relations and access to their notation.

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

  Substitution function. Replaces x in t with t'.

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

Notation for substitution.

Equations

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