class Subst (W : Type u_1) (Var : Type u_2) (E : outParam (Type u_3)) : Type (max (max u_1 u_2) u_3)

• subst : W → Var → E → W

  Written using a[x ↦ e]. Substitutes all x in a with e.

def «term__[__↦__]» : Lean.TrailingParserDescr

Written using a[x ↦ e]. Substitutes all x in a with e.

Equations

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

def Subst.substUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

@[implicit_reducible]

instance instSubstHashMap {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] : Subst (Std.HashMap α β) α β

Equations

• instSubstHashMap = { subst := fun (m : Std.HashMap α β) (x : α) (v : β) => m.insert x v }