def LeanSubst.List.rmap {S : Type} [i : RenMap S] (r : Ren) : List S → List S

Equations

• LeanSubst.List.rmap r [] = []
• LeanSubst.List.rmap r (x_1 :: tl) = LeanSubst.rmap r x_1 :: LeanSubst.List.rmap r tl

instance LeanSubst.instRenMapList {S : Type} [RenMap S] : RenMap (List S)

Equations

• LeanSubst.instRenMapList = { rmap := LeanSubst.List.rmap }

def LeanSubst.List.smap {S T : Type} [SubstMap S T] (σ : Subst T) : List S → List S

Equations

• LeanSubst.List.smap σ [] = []
• LeanSubst.List.smap σ (x_1 :: tl) = x_1[σ:_] :: LeanSubst.List.smap σ tl

instance LeanSubst.instSubstMapList {S T : Type} [SubstMap S T] : SubstMap (List S) T

Equations

• LeanSubst.instSubstMapList = { smap := LeanSubst.List.smap }

@[simp]

theorem LeanSubst.List.smap_nil {S T : Type} [SubstMap S T] {σ : Subst T} : [][σ:_] = []

@[simp]

theorem LeanSubst.List.smap_cons {S T : Type} [SubstMap S T] {x : S} {tl : List S} {σ : Subst T} : (x :: tl)[σ:_] = x[σ:_] :: tl[σ:_]

instance LeanSubst.instSubstMapIdList {S T : Type} [RenMap T] [SubstMap S T] [SubstMapId S T] : SubstMapId (List S) T

instance LeanSubst.instSubstMapComposeList {S T : Type} [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapCompose S T] : SubstMapCompose (List S) T

def LeanSubst.List.dep_subst_get {S T : Type} [SubstMap S T] (σ : Subst T) : List S → Nat → Option S

Equations

• LeanSubst.List.dep_subst_get σ [] x✝ = none
• LeanSubst.List.dep_subst_get σ (h :: tail) 0 = pure h[σ:_]
• LeanSubst.List.dep_subst_get σ (head :: t) n.succ = (LeanSubst.List.dep_subst_get σ t n)[σ:_]

@[reducible, inline]

abbrev LeanSubst.List.dep_subst_get1 {S : Type} [SubstMap S S] (σ : Subst S) : List S → Nat → Option S

Equations

• LeanSubst.List.dep_subst_get1 σ = LeanSubst.List.dep_subst_get σ

def LeanSubst.«term__[_|_:_]» : Lean.TrailingParserDescr

Equations

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

def LeanSubst.«term__[_|_]» : Lean.TrailingParserDescr

Equations

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

def LeanSubst.unexpand_list_dep_subst_get1 : Lean.PrettyPrinter.Unexpander

Equations

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

def LeanSubst.unexpand_list_dep_subst_get : Lean.PrettyPrinter.Unexpander

Equations

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

@[simp]

theorem LeanSubst.List.dep_subst_get_zero {S T : Type} [SubstMap S T] {σ : Subst T} {A : S} {Γ : List S} : dep_subst_get σ (A :: Γ) 0 = some A[σ:_]

@[simp]

theorem LeanSubst.List.dep_subst_get_succ {S T : Type} [SubstMap S T] {σ : Subst T} {A : S} {Γ : List S} {x : Nat} : dep_subst_get σ (A :: Γ) (x + 1) = (dep_subst_get σ Γ x)[σ:_]