@[reducible]

def LeanSubst.Subst.typeof {T : Type u2} : T → Type u2

Equations

• LeanSubst.Subst.typeof x✝ = T

@[reducible, inline]

abbrev LeanSubst.Var (T : Type u2) : Type

Equations

• LeanSubst.Var T = Nat

structure LeanSubst.Ren (T : Type u2) : Type u2

• act : Nat → Nat

inductive LeanSubst.RenUnit : Type u

• unit : RenUnit

@[instance_reducible]

def LeanSubst.RenVec : List (Type u2) → Type u2

Equations

• LeanSubst.RenVec [] = LeanSubst.RenUnit
• LeanSubst.RenVec (x_1 :: xs) = (LeanSubst.Ren x_1 × LeanSubst.RenVec xs)

def LeanSubst.RenVec.nil : RenVec []

Equations

• LeanSubst.RenVec.nil = LeanSubst.RenUnit.unit

class LeanSubst.RenSuffix (S : Type u1) (V : List (Type u2)) : Type

class LeanSubst.RenMap (S : Type u1) (V : List (Type u2)) : Type (max u1 u2)

• rmap : RenVec V → S → S

class inductive LeanSubst.RenMapAll : List (Type u2) → Type (u2 + 1)

• nil : RenMapAll []
• cons {V : Type u2} {Vs : List (Type u2)} [RenMap V [V]] [RenMap V Vs] [RenSuffix V Vs] : RenMapAll Vs → RenMapAll (V :: Vs)

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

Equations

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

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

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

@[instance_reducible]

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

Equations

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

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

Equations

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

structure LeanSubst.Subst (T : Type u2) : Type u2

• inner : Nat → Action T

inductive LeanSubst.SubstUnit : Type u

• unit : SubstUnit

@[instance_reducible]

def LeanSubst.SubstVec : List (Type u2) → Type u2

Equations

• LeanSubst.SubstVec [] = LeanSubst.SubstUnit
• LeanSubst.SubstVec (x_1 :: xs) = (LeanSubst.Subst x_1 × LeanSubst.SubstVec xs)

def LeanSubst.SubstVec.nil : SubstVec []

Equations

• LeanSubst.SubstVec.nil = LeanSubst.SubstUnit.unit

class LeanSubst.SubstAction (T : Type u1) (A : Type u2) (U : outParam (Type u3)) : Type (max (max u1 u2) u3)

• act (σ : Subst T) : A → U

def LeanSubst.Subst.act {S : Type u1} {T : Type u2} {U : Type u3} [SubstAction S T U] (σ : Subst S) : T → U

Equations

• σ.act = LeanSubst.SubstAction.act σ

@[instance_reducible]

instance LeanSubst.instSubstActionNatAction {T : Type u2} : SubstAction T Nat (Action T)

Equations

• LeanSubst.instSubstActionNatAction = { act := LeanSubst.Subst.inner }

class LeanSubst.SubstSuffix (S : Type u1) (V : List (Type u2)) : Type

class LeanSubst.SubstMap (S : Type u1) (V : List (Type u2)) : Type (max u1 u2)

• smap : SubstVec V → S → S

class inductive LeanSubst.SubstMapAll : List (Type u2) → Type (u2 + 1)

• nil : SubstMapAll []
• cons {V : Type u2} {Vs : List (Type u2)} [SubstMap V [V]] [SubstMap V Vs] [SubstSuffix V Vs] : SubstMapAll Vs → SubstMapAll (V :: Vs)

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

Equations

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