def LeanSubst.List.rmap {S : Type u1} {V : List (Type u2)} [RenMap S V] (r : RenVec V) : List S → List S

Equations

• LeanSubst.List.rmap r [] = []
• LeanSubst.List.rmap r (x_1 :: xs) = x_1⟨r,⟩ :: LeanSubst.List.rmap r xs

@[instance_reducible]

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

Equations

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

@[simp]

theorem LeanSubst.List.rmap_nil {S : Type u1} {V : List (Type u2)} [RenMap S V] {r : RenVec V} : []⟨r,⟩ = []

@[simp]

theorem LeanSubst.List.rmap_cons {S : Type u1} {V : List (Type u2)} [RenMap S V] {x : S} {xs : List S} {r : RenVec V} : (x :: xs)⟨r,⟩ = x⟨r,⟩ :: xs⟨r,⟩

instance LeanSubst.instRenMapIdList {S : Type u1} {V : List (Type u2)} [RenMap S V] [RenMapId S V] : RenMapId (List S) V

instance LeanSubst.instRenMapComposeList {S : Type u1} {V : List (Type u2)} [RenMap S V] [RenMapCompose S V] : RenMapCompose (List S) V

@[simp]

theorem LeanSubst.List.rmap_append {S : Type u1} {V : List (Type u2)} [RenMap S V] {xs ys : List S} {r : RenVec V} : (xs ++ ys)⟨r,⟩ = xs⟨r,⟩ ++ ys⟨r,⟩

@[simp]

theorem LeanSubst.List.rmap_get? {S : Type u1} {V : List (Type u2)} [RenMap S V] {x : List S} {n : Nat} {r : RenVec V} : x[n]?⟨r,⟩ = x⟨r,⟩[n]?

theorem LeanSubst.List.rmap_length {S : Type u1} {V : List (Type u2)} [RenMap S V] {x : List S} {r : RenVec V} : x⟨r,⟩.length = x.length

def LeanSubst.List.smap {S : Type u1} {V : List (Type u2)} [SubstMap S V] (σ : SubstVec V) : List S → List S

Equations

• LeanSubst.List.smap σ [] = []
• LeanSubst.List.smap σ (x_1 :: xs) = x_1[σ,] :: LeanSubst.List.smap σ xs

@[instance_reducible]

instance LeanSubst.instSubstMapList {S : Type u1} {V : List (Type u2)} [SubstMap S V] : SubstMap (List S) V

Equations

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

@[simp]

theorem LeanSubst.List.smap_none {S : Type u1} {V : List (Type u2)} [SubstMap S V] {σ : SubstVec V} : [][σ,] = []

@[simp]

theorem LeanSubst.List.smap_some {S : Type u1} {V : List (Type u2)} [SubstMap S V] {x : S} {xs : List S} {σ : SubstVec V} : (x :: xs)[σ,] = x[σ,] :: xs[σ,]

instance LeanSubst.instSubstMapIdListOfRenMap {S : Type u1} {V : List (Type u2)} [RenMap S V] [SubstMap S V] [SubstMapId S V] : SubstMapId (List S) V

instance LeanSubst.instSubstMapComposeList {S : Type u1} {V : List (Type u2)} [SubstMap S V] [SubstMapAll V] [SubstMapCompose S V] : SubstMapCompose (List S) V