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.

@[instance_reducible]

instance Cslib.HasSubstitution.instForallOfDecidableEq {α : Type u_1} {β : Type u_2} [DecidableEq α] : HasSubstitution (α → β) α β

Equations

• Cslib.HasSubstitution.instForallOfDecidableEq = { subst := Function.update }