def LeanSubst.Ren : Type

Equations

• LeanSubst.Ren = Sequ Nat

def LeanSubst.Ren.id : Ren

Equations

• LeanSubst.Ren.id x = x

def LeanSubst.Ren.lift (r : Ren) (k : Nat := 1) : Ren

Equations

• r.lift k x✝ = if x✝ < k then x✝ else r (x✝ - k) + k

class LeanSubst.RenMap (T : Type) : Type

• rmap : Ren → T → T

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 }

def LeanSubst.Subst (T : Type) : Type

Equations

• LeanSubst.Subst T = Sequ (LeanSubst.Subst.Action T)

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

Equations

• ↑x✝¹ x✝ = LeanSubst.re (x✝¹ x✝)

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

Equations

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

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

• smap : Subst T → S → S

def LeanSubst.Subst.lift {T : Type} [RenMap T] (σ : Subst T) (k : Nat := 1) : Subst T

Equations

• σ.lift k x✝ = if x✝ < k then LeanSubst.re x✝ else match σ (x✝ - k) with | LeanSubst.su t => LeanSubst.su t⟨fun (x : Nat) => x + k⟩ | LeanSubst.re i => LeanSubst.re (i + k)

@[reducible, inline]

abbrev LeanSubst.smap1 {S : Type} [SubstMap S S] : Subst S → S → S

Equations

• LeanSubst.smap1 = LeanSubst.smap

def LeanSubst.Subst.compose {T : Type} [RenMap T] [SubstMap T 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.hcompose {S T : Type} [RenMap T] [SubstMap S T] : Subst S → Subst T → Subst S

Equations

• (x✝² ◾ x✝¹) x✝ = match x✝² x✝ with | LeanSubst.su t => LeanSubst.su t[x✝¹:_] | LeanSubst.re k => LeanSubst.re 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+0@__» : Lean.ParserDescr

Equations

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

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

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

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

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

@[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} [RenMap T] [SubstMap T T] : +1 ∘ -1 = +0

@[simp]

theorem LeanSubst.Ren.lift_zero {r : Ren} : r.lift 0 = r

theorem LeanSubst.Ren.lift_succ {r : Ren} {k : Nat} : r.lift (k + 1) = (r.lift k).lift

@[simp]

theorem LeanSubst.Red.id_action {x : Nat} : Ren.id x = x

@[simp]

theorem LeanSubst.Ren.lift_id {k : Nat} : id.lift k = id

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

@[simp]

theorem LeanSubst.Ren.to_compose {T : Type} {r1 r2 : Ren} [RenMap T] [SubstMap T 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

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

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.«term_∘__1» : Lean.TrailingParserDescr

Equations

• LeanSubst.«term_∘__1» = Lean.ParserDescr.trailingNode `LeanSubst.«term_∘__1» 85 86 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘ ") (Lean.ParserDescr.cat `term 85))

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.unexpandRenApply : Lean.PrettyPrinter.Unexpander

Equations

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

def LeanSubst.unexpandSubstApply1 : Lean.PrettyPrinter.Unexpander

Equations

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

def LeanSubst.unexpandSubstApply : Lean.PrettyPrinter.Unexpander

Equations

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

instance LeanSubst.instHAndThenRen : HAndThen Ren Ren Ren

Equations

• LeanSubst.instHAndThenRen = { hAndThen := fun (f : LeanSubst.Ren) (g : Unit → LeanSubst.Ren) => g () ∘ f }

instance LeanSubst.instHAndThenForallNatRen : HAndThen (Nat → Nat) Ren Ren

Equations

• LeanSubst.instHAndThenForallNatRen = { hAndThen := fun (f : Nat → Nat) (g : Unit → LeanSubst.Ren) => g () ∘ f }

instance LeanSubst.instHAndThenRenForallNat : HAndThen Ren (Nat → Nat) Ren

Equations

• LeanSubst.instHAndThenRenForallNat = { hAndThen := fun (f : LeanSubst.Ren) (g : Unit → Nat → Nat) => g () ∘ f }

instance LeanSubst.instHAndThenSequNatRen : HAndThen (Sequ Nat) Ren Ren

Equations

• LeanSubst.instHAndThenSequNatRen = { hAndThen := fun (f : Sequ Nat) (g : Unit → LeanSubst.Ren) => g () ∘ f }

instance LeanSubst.instHAndThenRenSequNat : HAndThen Ren (Sequ Nat) Ren

Equations

• LeanSubst.instHAndThenRenSequNat = { hAndThen := fun (f : LeanSubst.Ren) (g : Unit → Sequ Nat) => g () ∘ f }

@[simp]

theorem LeanSubst.Ren.id_promote : (fun (x : Nat) => x) = id

@[simp]

theorem LeanSubst.Ren.post_compose_id_left {r : Ren} : id >> r = r

@[simp]

theorem LeanSubst.Ren.post_compose_id_right {r : Ren} : r >> id = r

@[simp]

theorem LeanSubst.Ren.post_compose_assoc {r1 r2 r3 : Ren} : (r1 >> r2) >> r3 = r1 >> r2 >> r3

@[simp]

theorem LeanSubst.Ren.post_compose_action {r1 r2 : Ren} {x : Nat} : (r1 >> r2) x = r2 (r1 x)

theorem LeanSubst.Ren.post_compose_lift_k1 {r1 r2 : Ren} : (r1 >> r2).lift = r1.lift >> r2.lift

@[simp]

theorem LeanSubst.Ren.post_compose_lift {k : Nat} {r1 r2 : Ren} : (r1 >> r2).lift k = r1.lift k >> r2.lift k