def HList : List (Type u) → Type u

Equations

• HList = List.foldr Prod PUnit

@[reducible, match_pattern, inline]

abbrev HList.nil : HList []

Equations

• HList.nil = PUnit.unit

@[reducible, match_pattern, inline]

abbrev HList.cons {τ : Type u_1} {τs : List (Type u_1)} (x : τ) (xs : HList τs) : HList (τ :: τs)

Equations

• x ::ₕ xs = (x, xs)

def HList.rec {motive : (τs : List (Type u)) → HList τs → Sort u} (nil : motive [] nil) (cons : {τ : Type u} → {τs : List (Type u)} → (x : τ) → (xs : HList τs) → motive τs xs → motive (τ :: τs) (x ::ₕ xs)) {τs : List (Type u)} (xs : HList τs) : motive τs xs

Equations

• HList.rec nil cons PUnit.unit = nil
• HList.rec nil cons (x, xs_2) = cons x xs_2 (HList.rec nil (fun {τ : Type ?u.255} {τs : List (Type ?u.255)} => cons) xs_2)

class HList.AllRepr (τs : List Type) : Type

• reprElems : HList τs → List Std.Format

@[implicit_reducible]

instance HList.instAllReprNil : AllRepr []

Equations

• HList.instAllReprNil = { reprElems := fun (x : HList []) => [] }

@[implicit_reducible]

instance HList.instAllReprConsOfRepr {τ : Type} {τs : List Type} [Repr τ] [AllRepr τs] : AllRepr (τ :: τs)

Equations

• HList.instAllReprConsOfRepr = { reprElems := fun (elms : HList (τ :: τs)) => match elms with | (x, xs) => repr x :: HList.AllRepr.reprElems xs }

@[implicit_reducible]

instance HList.instReprOfAllRepr {τs : List Type} [AllRepr τs] : Repr (HList τs)

Equations

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

@[implicit_reducible]

instance HList.instToStringOfAllRepr {τs : List Type} [AllRepr τs] : ToString (HList τs)

Equations

• HList.instToStringOfAllRepr = { toString := fun (xs : HList τs) => reprStr xs }

class HList.AllBEq (τs : List Type) : Type

• beqElems : HList τs → HList τs → Bool

@[implicit_reducible]

instance HList.instAllBEqNil : AllBEq []

Equations

• HList.instAllBEqNil = { beqElems := fun (x x_1 : HList []) => true }

@[implicit_reducible]

instance HList.instAllBEqConsOfBEq {τ : Type} {τs : List Type} [BEq τ] [AllBEq τs] : AllBEq (τ :: τs)

Equations

• HList.instAllBEqConsOfBEq = { beqElems := fun (xs ys : HList (τ :: τs)) => match xs, ys with | (x, xs), (y, ys) => x == y && HList.AllBEq.beqElems xs ys }

@[implicit_reducible]

instance HList.instBEqOfAllBEq {τs : List Type} [AllBEq τs] : BEq (HList τs)

Equations

• HList.instBEqOfAllBEq = { beq := fun (xs ys : HList τs) => HList.AllBEq.beqElems xs ys }

def HList.«term_::ₕ_» : Lean.TrailingParserDescr

Equations

• HList.«term_::ₕ_» = Lean.ParserDescr.trailingNode `HList.«term_::ₕ_» 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ::ₕ ") (Lean.ParserDescr.cat `term 67))

def HList.hlistCons : Lean.ParserDescr

Equations

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

def HList.length {τs : List (Type u)} : HList τs → Nat

Equations

• x✝.length = x✝¹.length

def HList.head {τ : Type u_1} {τs : List (Type u_1)} : HList (τ :: τs) → τ

Equations

• HList.head (x_1, snd) = x_1

def HList.tail {τ : Type u_1} {τs : List (Type u_1)} : HList (τ :: τs) → HList τs

Equations

• HList.tail (x_1, snd) = snd

def HList.get {τs : List (Type u)} (i : Fin τs.length) : HList τs → τs[i]

Equations

• HList.get ⟨0, isLt⟩ (x_3, xs) = x_3
• HList.get ⟨i.succ, hi⟩ (x_3, xs) = HList.get ⟨i, ⋯⟩ xs

@[reducible, inline]

abbrev HList.get' {τs : List (Type u)} (i : Nat) (h : i < τs.length := by decide) : HList τs → τs[i]

Equations

• HList.get' i h = HList.get ⟨i, h⟩

def HList.hAppend {αs βs : List (Type u)} : HList αs → HList βs → HList (αs ++ βs)

Equations

• HList.hAppend PUnit.unit x✝ = x✝
• HList.hAppend (x_5, xs) x✝ = (x_5, HList.hAppend xs x✝)

@[implicit_reducible]

instance HList.instHAppendHAppendListType {αs βs : List (Type u_1)} : HAppend (HList αs) (HList βs) (HList (αs ++ βs))

Equations

• HList.instHAppendHAppendListType = { hAppend := HList.hAppend }