class Subst (W Var E : 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.

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

Equations

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

instance WGCL.instSubstMem {D Var : Type} [DecidableEq Var] : Subst (Mem D Var) Var D

Equations

• WGCL.instSubstMem = { subst := fun (σ : WGCL.Mem D Var) (x : Var) (v : D) (y : Var) => if x = y then v else σ y }

instance WGCL.instSubstWeightingAExpr {D M Var : Type} [DecidableEq Var] : Subst (Weighting D M Var) Var (AExpr D Var)

Equations

• WGCL.instSubstWeightingAExpr = { subst := fun (f : WGCL.Weighting D M Var) (x : Var) (E : WGCL.AExpr D Var) (σ : WGCL.Mem D Var) => f σ[x ↦ E σ] }

@[simp]

theorem WGCL.Weighting.subst_mono {D M Var : Type} [DecidableEq Var] [Preorder M] {f₁ f₂ : Weighting D M Var} (h : f₁ ≤ f₂) (x : Var) (y : AExpr D Var) : f₁[x ↦ y] ≤ f₂[x ↦ y]