def LeanSubst.Ren : Type

Equations

• LeanSubst.Ren = Sequ Nat

def LeanSubst.Ren.lift : Ren → Ren

Equations

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

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

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

Equations

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

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.

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 → Subst T

Equations

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

@[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.to_lift {T : Type} [RenMap T] {r : Ren} : ↑r.lift = (↑r).lift

@[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

• LeanSubst.«term_∘_» = Lean.ParserDescr.trailingNode `LeanSubst.«term_∘_» 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.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.