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.

The noWs guard is intentional: substitution must be written as t[x := s], not t [x := s]. Without the guard, the term parser can attach a bracket from following syntax, such as an instance-binder field in a structure declaration, to the preceding term.

Equations

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

def Cslib.unexpandHasSubstitutionSubst : Lean.PrettyPrinter.Unexpander

Pretty-printer support for HasSubstitution.subst.

Equations

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