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

Equations

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

instance LeanSubst.instRenMapOption {S : Type} [RenMap S] : RenMap (Option S)

Equations

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

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

Equations

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

instance LeanSubst.instSubstMapOption {S T : Type} [SubstMap S T] : SubstMap (Option S) T

Equations

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

@[simp]

theorem LeanSubst.Option.smap_none {S T : Type} [SubstMap S T] {σ : Subst T} : none[σ:_] = none

@[simp]

theorem LeanSubst.Option.smap_some {S T : Type} [SubstMap S T] {x : S} {σ : Subst T} : (some x)[σ:_] = some x[σ:_]

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

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