class Subst (W Var : Type) (E : outParam Type) : Type

• 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} [BEq α] [Hashable α] : Subst (Std.HashMap α β) α β

Equations

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