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

Equations

• LeanSubst.Option.rmap r none = none
• LeanSubst.Option.rmap r (some t) = some t⟨r,⟩

@[instance_reducible]

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

Equations

• LeanSubst.instRenMapOption = { rmap := LeanSubst.Option.rmap }

@[simp]

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

@[simp]

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

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

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

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

Equations

• LeanSubst.Option.smap σ none = none
• LeanSubst.Option.smap σ (some t) = some t[σ,]

@[instance_reducible]

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

Equations

• LeanSubst.instSubstMapOption = { smap := LeanSubst.Option.smap }

@[simp]

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

@[simp]

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

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

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