def LeanSubst.Sequence.cons {T : Sort u_1} (x : T) (xs : Nat → T) : Nat → T

Equations

• (x::xs) 0 = x
• (x::xs) n.succ = xs n

def LeanSubst.«term_::_» : Lean.TrailingParserDescr

Equations

• LeanSubst.«term_::_» = Lean.ParserDescr.trailingNode `LeanSubst.«term_::_» 55 56 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "::") (Lean.ParserDescr.cat `term 55))

def LeanSubst.Ren : Type

Equations

• LeanSubst.Ren = (Nat → Nat)

inductive LeanSubst.Subst.Action (T : Type u) : Type u

• re {T : Type u} : Nat → Action T
• su {T : Type u} : T → Action T

instance LeanSubst.Subst.instPrefixHash_Action {T : Type u} : PrefixHash (Action T)

Equations

• LeanSubst.Subst.instPrefixHash_Action = { hash := LeanSubst.Subst.Action.re }

instance LeanSubst.Subst.instPrefixPercent_Action {T : Type u} : PrefixPercent T Action

Equations

• LeanSubst.Subst.instPrefixPercent_Action = { percent := LeanSubst.Subst.Action.su }

@[simp]

theorem LeanSubst.Subst.re_def {T : Type u} {k : Nat} : Action.re k = #k

@[simp]

theorem LeanSubst.Subst.re_eq {T : Type u} {k1 k2 : Nat} : (#k1 = #k2) = (k1 = k2)

@[simp]

theorem LeanSubst.Subst.su_def {T : Type u} {t : T} : Action.su t = %t

@[simp]

theorem LeanSubst.Subst.su_eq {T : Type u} {t1 t2 : T} : (%t1 = %t2) = (t1 = t2)

def LeanSubst.Subst.Lift (X : Type u) : Type u

Equations

• LeanSubst.Subst.Lift X = ((Nat → LeanSubst.Subst.Action X) → Nat → LeanSubst.Subst.Action X)

def LeanSubst.Subst (T : Type u) : Type u

Equations

• LeanSubst.Subst T = (Nat → LeanSubst.Subst.Action T)

class LeanSubst.SubstMap (T : Type u) : Type u

• smap : Subst.Lift T → (Nat → Subst.Action T) → T → T

def LeanSubst.Ren.to {T : Type u} : Ren → Subst T

Equations

• x✝¹.to x✝ = LeanSubst.Subst.Action.re (x✝¹ x✝)

def LeanSubst.Ren.fro {T : Type u} : Subst T → Ren

Equations

• LeanSubst.Ren.fro x✝¹ x✝ = match x✝¹ x✝ with | LeanSubst.Subst.Action.su a => 0 | LeanSubst.Subst.Action.re k => k

def LeanSubst.Ren.lift : Ren → Ren

Equations

• x✝.lift 0 = 0
• x✝.lift n.succ = x✝ n + 1

def LeanSubst.Ren.apply {T : Type u} [SubstMap T] (r : Ren) : T → T

Equations

• r.apply = LeanSubst.SubstMap.smap (LeanSubst.Ren.to ∘ LeanSubst.Ren.lift ∘ LeanSubst.Ren.fro) r.to

def LeanSubst.Subst.lift {T : Type u} [SubstMap T] : Subst T → Subst T

Equations

• One or more equations did not get rendered due to their size.
• x✝.lift 0 = LeanSubst.Subst.Action.re 0

def LeanSubst.Subst.apply {T : Type u} [SubstMap T] (σ : Subst T) : T → T

Equations

• σ.apply = LeanSubst.SubstMap.smap LeanSubst.Subst.lift σ

def LeanSubst.Subst.compose {T : Type u} [SubstMap T] : Subst T → Subst T → Subst T

Equations

• (x✝² ∘ x✝¹) x✝ = match x✝² x✝ with | LeanSubst.Subst.Action.su t => LeanSubst.Subst.Action.su (t[x✝¹]) | LeanSubst.Subst.Action.re k => x✝¹ k

def LeanSubst.I {T : Type u} : Subst T

Equations

• LeanSubst.I n = #n

def LeanSubst.S {T : Type u} : Subst T

Equations

• LeanSubst.S n = #(n + 1)

def LeanSubst.Sn {T : Type u} (k : Nat) : Subst T

Equations

• LeanSubst.Sn k n = #(n + k)

@[simp]

theorem LeanSubst.I_action {T : Type u} {n : Nat} : I n = #n

@[simp]

theorem LeanSubst.S_action {T : Type u} {n : Nat} : S n = #(n + 1)

@[simp]

theorem LeanSubst.Sn_action {T : Type u} {k n : Nat} : Sn k n = #(n + k)

@[simp]

theorem LeanSubst.to_I {T : Type u} : (Ren.to fun (x : Nat) => x) = I

@[simp]

theorem LeanSubst.to_S {T : Type u} : (Ren.to fun (x : Nat) => x + 1) = S

@[simp]

theorem LeanSubst.to_Sn {T : Type u} {k : Nat} : (Ren.to fun (x : Nat) => x + k) = Sn k

def LeanSubst.«term_[_]» : Lean.TrailingParserDescr

Equations

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

def LeanSubst.«term_∘_» : Lean.TrailingParserDescr

Equations

• LeanSubst.«term_∘_» = Lean.ParserDescr.trailingNode `LeanSubst.«term_∘_» 65 66 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘ ") (Lean.ParserDescr.cat `term 65))

class LeanSubst.SubstMapStable (T : Type u) [SubstMap T] : Prop

• apply_id {t : T} : t[I] = t
• apply_stable {r : Ren} {σ : Subst T} : r.to = σ → r.apply = σ.apply

class LeanSubst.SubstMapCompose (T : Type u) [SubstMap T] : Prop

• apply_compose {s : T} {σ τ : Subst T} : s[σ][τ] = s[σ ∘ τ]

theorem LeanSubst.Ren.lift_to_commute {T : Type u} [SubstMap T] {r : Ren} : r.lift.to = r.to.lift

@[simp]

theorem LeanSubst.Subst.rewrite1 {T : Type u} : #0::S = I

@[simp]

theorem LeanSubst.Subst.I_lift {T : Type u} [SubstMap T] : I.lift = I

@[simp]

theorem LeanSubst.Subst.rewrite2 {T : Type u} [SubstMap T] {σ : Subst T} : I ∘ σ = σ

@[simp]

theorem LeanSubst.Subst.rewrite3_replace {T : Type u} [SubstMap T] {σ τ : Subst T} {s : T} : (%s::σ) ∘ τ = %(s[τ])::σ ∘ τ

@[simp]

theorem LeanSubst.Subst.rewrite3_rename {T : Type u} [SubstMap T] {s : Nat} {σ τ : Subst T} : (#s::σ) ∘ τ = τ s::σ ∘ τ

@[simp]

theorem LeanSubst.Subst.rewrite4 {T : Type u} [SubstMap T] {s : Action T} {σ : Subst T} : S ∘ (s::σ) = σ

@[simp]

theorem LeanSubst.Subst.rewrite5 {T : Type u} [SubstMap T] {σ : Subst T} : σ 0::S ∘ σ = σ

@[simp]

theorem LeanSubst.Subst.apply_I_is_id {T : Type u} [SubstMap T] [SubstMapStable T] {s : T} : s[I] = s

@[simp]

theorem LeanSubst.Subst.rewrite_lift {T : Type u} [SubstMap T] [SubstMapStable T] {σ : Subst T} : σ.lift = #0::σ ∘ S

@[simp]

theorem LeanSubst.Subst.rewrite6 {T : Type u} [SubstMap T] [SubstMapStable T] {σ : Subst T} : σ ∘ I = σ

@[simp]

theorem LeanSubst.Subst.apply_compose_commute {T : Type u} [SubstMap T] [SubstMapCompose T] {s : T} {σ τ : Subst T} : s[σ][τ] = s[σ ∘ τ]

@[simp]

theorem LeanSubst.Subst.rewrite7 {T : Type u} [SubstMap T] [SubstMapCompose T] {σ τ μ : Subst T} : (σ ∘ τ) ∘ μ = σ ∘ τ ∘ μ

def LeanSubst.«tacticSolve_stable_,_» : Lean.ParserDescr

Equations

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

def LeanSubst.«tacticSolve_compose_,_,_,_» : Lean.ParserDescr

Equations

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