def LeanSubst.Sequence.cons {T : Type u} (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))

@[reducible, inline]

abbrev LeanSubst.Ren : Type

Equations

• LeanSubst.Ren = (Nat → Nat)

inductive LeanSubst.Subst.Kind : Type

• re : Kind
• su : Kind

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

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

def LeanSubst.Subst.instReprAction.repr {T✝ : Type} [Repr T✝] : Action T✝ → Nat → Std.Format

Equations

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

instance LeanSubst.Subst.instReprAction {T✝ : Type} [Repr T✝] : Repr (Action T✝)

Equations

• LeanSubst.Subst.instReprAction = { reprPrec := LeanSubst.Subst.instReprAction.repr }

@[reducible, inline]

abbrev LeanSubst.Subst (T : Type) : Type

Equations

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

def LeanSubst.SplitSubst (T : Type) : Subst.Kind → Type

Equations

• LeanSubst.SplitSubst T LeanSubst.Subst.Kind.re = LeanSubst.Ren
• LeanSubst.SplitSubst T LeanSubst.Subst.Kind.su = LeanSubst.Subst T

@[reducible, inline]

abbrev LeanSubst.Subst.Lift (T : Type) (k : Kind) : Type

Equations

• LeanSubst.Subst.Lift T k = (LeanSubst.SplitSubst T k → LeanSubst.SplitSubst T k)

class LeanSubst.SubstMap (T : Type) : Type

• smap (k : Subst.Kind) : Subst.Lift T k → SplitSubst T k → T → T

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

Equations

• ↑x✝ = fun (n : Nat) => LeanSubst.re (x✝ n)

instance LeanSubst.instCoe_Ren_Subst {T : Type} : Coe Ren (Subst T)

Equations

• LeanSubst.instCoe_Ren_Subst = { coe := LeanSubst.Ren.to }

def LeanSubst.Ren.lift : Ren → Ren

Equations

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

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

Equations

• r.apply = LeanSubst.SubstMap.smap LeanSubst.Subst.Kind.re LeanSubst.Ren.lift r

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

Equations

• x✝.lift 0 = LeanSubst.re 0
• x✝.lift n.succ = match x✝ n with | LeanSubst.su t => LeanSubst.su (LeanSubst.Ren.apply (fun (n : Nat) => n + 1) t) | LeanSubst.re k => LeanSubst.re (k + 1)

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

Equations

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

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

Equations

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

def LeanSubst.Subst.id {T : Type} : Subst T

Equations

• +0 n = LeanSubst.re n

def LeanSubst.Subst.succ {T : Type} : Subst T

Equations

• +1 n = LeanSubst.re (n + 1)

def LeanSubst.Subst.pred {T : Type} : Subst T

Equations

• -1 n = LeanSubst.re (n - 1)

def LeanSubst.«term+0» : Lean.ParserDescr

Equations

• LeanSubst.«term+0» = Lean.ParserDescr.node `LeanSubst.«term+0» 1024 (Lean.ParserDescr.symbol "+0")

def LeanSubst.«term+1» : Lean.ParserDescr

Equations

• LeanSubst.«term+1» = Lean.ParserDescr.node `LeanSubst.«term+1» 1024 (Lean.ParserDescr.symbol "+1")

def LeanSubst.«term-1» : Lean.ParserDescr

Equations

• LeanSubst.«term-1» = Lean.ParserDescr.node `LeanSubst.«term-1» 1024 (Lean.ParserDescr.symbol "-1")

@[simp]

theorem LeanSubst.Subst.id_action {T : Type} {n : Nat} : +0 n = re n

@[simp]

theorem LeanSubst.Subst.succ_action {T : Type} {n : Nat} : +1 n = re (n + 1)

@[simp]

theorem LeanSubst.Subst.pred_action {T : Type} {n : Nat} : -1 n = re (n - 1)

@[simp]

theorem LeanSubst.Ren.to_id {T : Type} : ↑id = +0

@[simp]

theorem LeanSubst.Ren.to_succ {T : Type} : (↑fun (x : Nat) => x + 1) = +1

@[simp]

theorem LeanSubst.Ren.to_pred {T : Type} : (↑fun (x : Nat) => x - 1) = -1

@[simp]

theorem LeanSubst.Ren.pred_succ {T : Type} [SubstMap T] : +1 ∘ -1 = +0

@[simp]

theorem LeanSubst.Ren.to_compose {T : Type} {r1 r2 : Ren} [SubstMap T] : ↑(r2 ∘ r1) = ↑r1 ∘ ↑r2

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_∘_» 85 86 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘ ") (Lean.ParserDescr.cat `term 85))

def LeanSubst.unexpandSubstApply : Lean.PrettyPrinter.Unexpander

Equations

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

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

• apply_id {t : T} : t[+0] = t
• apply_stable (r : Ren) (σ : Subst T) : ↑r = σ → r.apply = σ.apply

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

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

theorem LeanSubst.Ren.to_lift {T : Type} [SubstMap T] {r : Ren} : ↑r.lift = (↑r).lift

theorem LeanSubst.Ren.lift_eq_from_eq {T : Type} [SubstMap T] {r : Ren} {σ : Subst T} : ↑r = σ → ↑r.lift = σ.lift

@[simp]

theorem LeanSubst.Subst.rewrite1 {T : Type} : re 0::+1 = +0

@[simp]

theorem LeanSubst.Subst.I_lift {T : Type} [SubstMap T] : +0.lift = +0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LeanSubst.Subst.rewrite_lift {T : Type} [SubstMap T] [SubstMapStable T] {σ : Subst T} : σ.lift = re 0::σ ∘ +1

@[simp]

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

@[simp]

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

@[simp]

theorem LeanSubst.Subst.rewrite7 {T : Type} [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.