class Substitution (α : Type u_1) {ι : outParam (Type u_2)} (β : outParam (ι → Type u_3)) : Type (max (max u_1 u_2) u_3)

• subst : α → Sigma β → α

@[implicit_reducible]

instance Substitution.instHashMap {ι : Type u_1} {β : Type u_2} [BEq ι] [Hashable ι] : Substitution (Std.HashMap ι β) fun (x : ι) => β

Equations

• Substitution.instHashMap = { subst := fun (map : Std.HashMap ι β) => Sigma.uncurry map.insert }

def Substitution.substs {α : Type u_1} {ι✝ : outParam (Type u_2)} {β : ι✝ → Type u_3} [Substitution α β] (m : α) (xs : List (Sigma β)) : α

Equations

• m[..xs] = List.foldr (fun (b : Sigma β) (acc : α) => Substitution.subst acc b) m xs

def Lean.Parser.Category.substitution_arg : Category

Equations

• Lean.Parser.Category.substitution_arg = { }

def Substitution.substitution_arg.quot : Lean.ParserDescr

Equations

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

def Substitution.«substitution_arg__↦__» : Lean.ParserDescr

Equations

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

def Substitution.«substitution_arg.._» : Lean.ParserDescr

Equations

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

def Substitution.«term__[_]» : Lean.TrailingParserDescr

Equations

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

def Substitution.substsUnexpander : Lean.PrettyPrinter.Unexpander

Equations

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

@[simp]

theorem Substitution.substs_nil {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [Substitution α β] {m : α} : m[] = m

theorem Substitution.substs_cons {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [Substitution α β] {m : α} {x : Sigma β} {xs : List (Sigma β)} : m[..x :: xs] = subst (m[..xs]) x

theorem Substitution.substs_cons_substs {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [Substitution α β] {m : α} {x : Sigma β} {xs : List (Sigma β)} : m[..x :: xs] = m[..xs][..[x]]

theorem Substitution.substs_append {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [Substitution α β] {m : α} {xs ys : List (Sigma β)} : m[..xs ++ ys] = m[..ys][..xs]

theorem Substitution.subst_singleton {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [Substitution α β] {m : α} {x : Sigma β} : m[..[x]] = subst m x

theorem Substitution.substs_of_binary {α₁ : Type u_4} {α₂ : Type u_5} {α₃ : Type u_6} {ι : Type u_7} {β : ι → Type u_8} [Substitution α₁ β] [Substitution α₂ β] [Substitution α₃ β] {m : α₁} {n : α₂} {xs : List (Sigma β)} {f : α₁ → α₂ → α₃} (h : ∀ (m : α₁) (n : α₂) (b : Sigma β), (f m n)[..[b]] = f (m[..[b]]) (n[..[b]])) : (f m n)[..xs] = f (m[..xs]) (n[..xs])

def Substitution.IsIndepPair {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [Substitution α β] (m : α) (x : ι) : Prop

Equations

• Substitution.IsIndepPair m x = ∀ (v : β x), m[x ↦ v] = m

class Substitution.IndepPair {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [Substitution α β] (m : α) (x : ι) : Prop

• is_indep : IsIndepPair m x

theorem Substitution.indepPair_iff {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [Substitution α β] (m : α) (x : ι) : IndepPair m x ↔ IsIndepPair m x

@[simp]

theorem Substitution.indep_pair {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [Substitution α β] {m : α} {x : ι} (h : IsIndepPair m x) {v : β x} : m[x ↦ v] = m

structure Substitution.Example.Context (𝒱 : Type u_4) : Type (max u_4 (u_5 + 1))

• types : 𝒱 → Type u_5

@[reducible, inline]

abbrev Substitution.Example.Context.Mem {𝒱 : Type u_4} (Γ : Context 𝒱) : Type (max u_4 u_5)

Equations

• Γ.Mem = ((v : 𝒱) → Γ.types v)

@[implicit_reducible]

instance Substitution.Example.instMemTypes {𝒱 : Type u_4} {Γ : Context 𝒱} [DecidableEq 𝒱] : Substitution Γ.Mem Γ.types

Equations

• Substitution.Example.instMemTypes = { subst := fun (σ : Γ.Mem) => Sigma.uncurry fun (x : 𝒱) (e : Γ.types x) (y : 𝒱) => if h : x = y then h ▸ e else σ y }

@[implicit_reducible]

instance Substitution.Example.instForallMemForallTypes {𝒱 : Type u_4} {α : Type u_5} {Γ : Context 𝒱} [DecidableEq 𝒱] : Substitution (Γ.Mem → α) fun (x : 𝒱) => Γ.Mem → Γ.types x

Equations

• Substitution.Example.instForallMemForallTypes = { subst := fun (X : Γ.Mem → α) => Sigma.uncurry fun (v : 𝒱) (e : Γ.Mem → Γ.types v) (σ : Γ.Mem) => X (σ[v ↦ e σ]) }