inductive Auto.HList {α : Type u_1} (β : α → Sort u_2) : List α → Sort (max (u_1 + 1) u_2)

• nil {α : Type u_1} {β : α → Sort u_2} : HList β []
• cons {α : Type u_1} {β : α → Sort u_2} {ty : α} {tys : List α} (x : β ty) : HList β tys → HList β (ty :: tys)

@[irreducible]

def Auto.HList.nil_IsomType {α : Type u} {β : α → Sort v} : IsomType (HList β []) PUnit

Equations

• Auto.HList.nil_IsomType = { f := fun (x : Auto.HList β []) => PUnit.unit, g := fun (x : PUnit) => Auto.HList.nil, eq₁ := ⋯, eq₂ := ⋯ }

@[irreducible]

def Auto.HList.cons_IsomType {α : Type u} {β : α → Type v} {a : α} {as : List α} : IsomType (HList β (a :: as)) (β a × HList β as)

Equations

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

@[irreducible]

def Auto.HList.singleton_IsomType {α : Type u_1} {β : α → Sort u_2} {a : α} : IsomType (HList β [a]) (β a)

Equations

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

def Auto.HList.getD {α : Type u_1} {β : α → Sort u_2} {ty : α} (default : β ty) {tys : List α} : HList β tys → (n : Nat) → β (tys.getD n ty)

Equations

• Auto.HList.getD default Auto.HList.nil x✝ = default
• Auto.HList.getD default (Auto.HList.cons a a_1) 0 = a
• Auto.HList.getD default (Auto.HList.cons x_3 as) n.succ = Auto.HList.getD default as n

theorem Auto.HList.getD_heq {α₁ α₂ : Type u_1} {β₁ : α₁ → Sort u_2} {ty₁ : α₁} {default₁ : β₁ ty₁} {tys₁ : List α₁} {hl₁ : HList β₁ tys₁} {n₁ : Nat} {β₂ : α₂ → Sort u_2} {ty₂ : α₂} {default₂ : β₂ ty₂} {tys₂ : List α₂} {hl₂ : HList β₂ tys₂} {n₂ : Nat} (hβ : β₁ ≍ β₂) (hty : ty₁ ≍ ty₂) (hdefault : default₁ ≍ default₂) (htys : tys₁ ≍ tys₂) (hhl : hl₁ ≍ hl₂) (hn : n₁ = n₂) : getD default₁ hl₁ n₁ ≍ getD default₂ hl₂ n₂

def Auto.HList.ofMapTy {β : Type u_1} {α : Type u_2} {γ : β → Sort u_3} (f : α → β) {tys : List α} : HList γ (List.map f tys) → HList (γ ∘ f) tys

Equations

• Auto.HList.ofMapTy f Auto.HList.nil = Auto.HList.nil
• Auto.HList.ofMapTy f (Auto.HList.cons x_2 xs) = Auto.HList.cons x_2 (Auto.HList.ofMapTy f xs)

def Auto.HList.toMapTy {β : Type u_1} {α : Type u_2} {γ : β → Sort u_3} (f : α → β) {tys : List α} : HList (γ ∘ f) tys → HList γ (List.map f tys)

Equations

• Auto.HList.toMapTy f Auto.HList.nil = Auto.HList.nil
• Auto.HList.toMapTy f (Auto.HList.cons x_2 xs) = Auto.HList.cons x_2 (Auto.HList.toMapTy f xs)

def Auto.HList.ofMapList {α : Type u_1} {β : α → Sort u_2} (f : (x : α) → β x) (xs : List α) : HList β xs

Equations

• Auto.HList.ofMapList f [] = Auto.HList.nil
• Auto.HList.ofMapList f (x_1 :: xs) = Auto.HList.cons (f x_1) (Auto.HList.ofMapList f xs)

def Auto.HList.map {α : Type u_1} {β : α → Sort u_2} {γ : α → Sort u_3} (f : (a : α) → β a → γ a) {tys : List α} (xs : HList β tys) : HList γ tys

Equations

• Auto.HList.map f Auto.HList.nil = Auto.HList.nil
• Auto.HList.map f (Auto.HList.cons x_2 xs) = Auto.HList.cons (f head x_2) (Auto.HList.map f xs)

def Auto.HList.append {α✝ : Type u_1} {β : α✝ → Sort u_2} {as bs : List α✝} (xs : HList β as) (ys : HList β bs) : HList β (as ++ bs)

Equations

• Auto.HList.nil.append x✝ = x✝
• (Auto.HList.cons x_2 xs).append x✝ = Auto.HList.cons x_2 (xs.append x✝)

theorem Auto.HList.append_assoc {α✝ : Type u_1} {β : α✝ → Sort u_2} {as bs cs : List α✝} (xs : HList β as) (ys : HList β bs) (zs : HList β cs) : (xs.append ys).append zs ≍ xs.append (ys.append zs)

theorem Auto.HList.getD_append_left {α✝ : Type u_1} {β : α✝ → Sort u_2} {as bs : List α✝} {i : Nat} {a✝ : α✝} {df : β a✝} (xs : HList β as) (ys : HList β bs) (h : i < as.length) : getD df (xs.append ys) i ≍ getD df xs i

theorem Auto.HList.getD_append_right {α✝ : Type u_1} {β : α✝ → Sort u_2} {as bs : List α✝} {i : Nat} {a✝ : α✝} {df : β a✝} (xs : HList β as) (ys : HList β bs) (h : i ≥ as.length) : getD df (xs.append ys) i ≍ getD df ys (i - as.length)

def Auto.HList.append_get_left {α✝ : Type u_1} {β : α✝ → Sort u_2} {as bs : List α✝} (xs : HList β (as ++ bs)) : HList β as

Equations

• x.append_get_left = Auto.HList.nil
• (Auto.HList.cons x xs_3).append_get_left = Auto.HList.cons x xs_3.append_get_left

def Auto.HList.append_get_right {α✝ : Type u_1} {β : α✝ → Sort u_2} {as bs : List α✝} (xs : HList β (as ++ bs)) : HList β bs

Equations

• x.append_get_right = x
• (Auto.HList.cons x xs_3).append_get_right = xs_3.append_get_right

theorem Auto.HList.append_get_left_eq {α✝ : Type u_1} {β : α✝ → Sort u_2} {as bs : List α✝} (xs : HList β as) (ys : HList β bs) : (xs.append ys).append_get_left = xs

theorem Auto.HList.append_get_right_eq {α✝ : Type u_1} {β : α✝ → Sort u_2} {as bs : List α✝} (xs : HList β as) (ys : HList β bs) : (xs.append ys).append_get_right = ys

theorem Auto.HList.append_get_append_eq {α✝ : Type u_1} {β : α✝ → Sort u_2} {as bs : List α✝} (xs : HList β (as ++ bs)) : xs.append_get_left.append xs.append_get_right = xs

@[irreducible]

def Auto.HList.append_IsomType {α : Type u} {β : α → Sort v} {xs ys : List α} : IsomType (HList β (xs ++ ys)) (HList β xs ×' HList β ys)

Equations

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

@[irreducible]

def Auto.HList.append_singleton_IsomType {α : Type u} {β : α → Sort v} {xs : List α} {x : α} : IsomType (HList β (xs ++ [x])) (HList β xs ×' β x)

Equations

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

def Auto.HList.reverseAux {α✝ : Type u_1} {β : α✝ → Sort u_2} {bs as : List α✝} (xs : HList β as) (ys : HList β bs) : HList β (as.reverseAux bs)

Equations

• Auto.HList.nil.reverseAux x✝ = x✝
• (Auto.HList.cons x_3 xs).reverseAux x✝ = xs.reverseAux (Auto.HList.cons x_3 x✝)

def Auto.HList.reverse {α✝ : Type u_1} {β : α✝ → Sort u_2} {as : List α✝} (xs : HList β as) : HList β as.reverse

Equations

• xs.reverse = xs.reverseAux Auto.HList.nil

theorem Auto.HList.reverse_nil {α✝ : Type u_1} {β : α✝ → Sort u_2} : nil.reverse = nil

theorem Auto.HList.reverseAux_eq_append {α✝ : Type u_1} {β : α✝ → Sort u_2} {as bs : List α✝} {xs : HList β as} {ys : HList β bs} : xs.reverseAux ys ≍ (xs.reverseAux nil).append ys

theorem Auto.HList.reverse_cons {α✝ : Type u_1} {β : α✝ → Sort u_2} {as : List α✝} {a : α✝} {x : β a} {xs : HList β as} : (cons x xs).reverse ≍ xs.reverse.append (cons x nil)