inductive LeanSubst.Ctx (T : Type) : Type

• nil {T : Type} : Ctx T
• cons {T : Type} : T → Ctx T → Ctx T

def LeanSubst.«term[]» : Lean.ParserDescr

Equations

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

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

Equations

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

def LeanSubst.nth {T : Type} [Inhabited T] : Ctx T → Nat → T

Equations

• LeanSubst.nth [] x✝ = default
• LeanSubst.nth (h::a) 0 = h
• LeanSubst.nth (a::t) n.succ = LeanSubst.nth t n

def LeanSubst.Ctx.dnth {T : Type} [Inhabited T] [SubstMap T] : Ctx T → Nat → T

Equations

• [].dnth x✝ = default
• (h::a).dnth 0 = h[+1]
• (a::t).dnth n.succ = (t.dnth n)[+1]

instance LeanSubst.instGetElemCtxNatTrue {T : Type} [Inhabited T] [SubstMap T] : GetElem (Ctx T) Nat T fun (x : Ctx T) (x_1 : Nat) => True

Equations

• LeanSubst.instGetElemCtxNatTrue = { getElem := fun (Γ : LeanSubst.Ctx T) (x : Nat) (x_1 : True) => Γ.dnth x }

@[simp]

theorem LeanSubst.Ctx.elem_cons_zero {T : Type} [Inhabited T] [SubstMap T] {A : T} {Γ : Ctx T} : (A::Γ)[0] = A[+1]

@[simp]

theorem LeanSubst.Ctx.elem_cons_succ {T : Type} [Inhabited T] [SubstMap T] {A : T} {Γ : Ctx T} {x : Nat} : (A::Γ)[x + 1] = Γ[x][+1]