inductive HVector {α : Type u_1} (f : α → Type u_2) : List α → Type (max u_1 u_2)

An heterogeneous vector

• nil: {α : Type u_1} → {f : α → Type u_2} → HVector f []
• cons: {α : Type u_1} → {f : α → Type u_2} → {as : List α} → {a : α} → f a → HVector f as → HVector f (a :: as)

instance HVector.decidableEq {α : Type u_3} {A : α → Type u_1} [(a : α) → DecidableEq (A a)] {l : List α} : DecidableEq (HVector A l)

Equations

• HVector.nil.decidableEq HVector.nil = isTrue ⋯
• (x₁::ₕv₁).decidableEq (x₂::ₕv₂) = decidable_of_iff (x₁ = x₂ ∧ v₁ = v₂) ⋯

def HVector.head {α : Type u_3} {A : α → Type u_1} {as : List α} {a : α} : HVector A (a :: as) → A a

Equations

• (x_1::ₕa_1).head = x_1

def HVector.tail {α : Type u_3} {A : α → Type u_1} {as : List α} {a : α} : HVector A (a :: as) → HVector A as

Equations

• (x_1::ₕa_1).tail = a_1

def HVector.map {α : Type u_3} {A : α → Type u_1} {B : α → Type u_2} (f : (a : α) → A a → B a) {l : List α} : HVector A l → HVector B l

Equations

• HVector.map f HVector.nil = HVector.nil
• HVector.map f (a::ₕas) = (f t a::ₕHVector.map f as)

def HVector.map' {α : Type u_5} {β : Type u_6} {A : α → Type u_3} {B : β → Type u_4} (f' : α → β) (f : (a : α) → A a → B (f' a)) {l : List α} : HVector A l → HVector B (List.map f' l)

An alternative to map which also maps a function over the index list

Equations

• HVector.map' f' f HVector.nil = HVector.nil
• HVector.map' f' f (a::ₕas) = (f t a::ₕHVector.map' f' f as)

def HVector.foldl {α : Type u_4} {A : α → Type u_1} {B : Type u_3} (f : (a : α) → B → A a → B) {l : List α} : B → HVector A l → B

Equations

• HVector.foldl f x HVector.nil = x
• HVector.foldl f x (a::ₕas) = HVector.foldl f (f t x a) as

def HVector.get {α : Type u_3} {A : α → Type u_1} {as : List α} : HVector A as → (i : Fin as.length) → A (as.get i)

Equations

• HVector.nil.get i = i.elim0
• (x_2::ₕa).get ⟨0, isLt⟩ = x_2
• (a::ₕxs).get ⟨i.succ, h⟩ = xs.get ⟨i, ⋯⟩

def HVector.tacticHvector_get_elem_tactic : Lean.ParserDescr

To be used as an auto-tactic to prove that the index of getN is within bounds

Equations

• HVector.tacticHvector_get_elem_tactic = Lean.ParserDescr.node `HVector.tacticHvector_get_elem_tactic 1024 (Lean.ParserDescr.nonReservedSymbol "hvector_get_elem_tactic" false)

@[reducible, inline]

abbrev HVector.getN {α : Type u_3} {A : α → Type u_1} {as : List α} (x : HVector A as) (i : Nat) (hi : autoParam (i < as.length) _auto✝) : A (as.get ⟨i, hi⟩)

x.getN i indexes into a HVector with a Nat.

Note that we cannot define a proper instance of GetElem for HVector, since GetElem requires us to specify a type elem such that xs[i] : elem, but elem is not allowed to depend on the concrete index i. Thus, GetElem does not properly support heterogeneous container types like HVector

Equations

• x.getN i hi = x.get ⟨i, hi⟩

def HVector.ToTupleType {α : Type u_4} (A : α → Type u_3) : List α → Type u_3

Equations

• HVector.ToTupleType A [] = PUnit
• HVector.ToTupleType A [a] = A a
• HVector.ToTupleType A (a :: as) = (A a × HVector.ToTupleType A as)

def HVector.toTuple {α : Type u_3} {A : α → Type u_1} {as : List α} : HVector A as → HVector.ToTupleType A as

Turns a HVector A [a₁, a₂, ..., aₙ] into a tuple (A a₁) × (A a₂) × ... × (A aₙ)

Equations

• HVector.nil.toTuple = PUnit.unit
• (x_1::ₕHVector.nil).toTuple = x_1
• (x₁::ₕ(x₂::ₕxs)).toTuple = (x₁, (x₂::ₕxs).toTuple)

@[reducible, inline]

abbrev HVector.toSingle {α : Type u_3} {A : α → Type u_1} {a₁ : α} : HVector A [a₁] → A a₁

Equations

• HVector.toSingle = HVector.toTuple

@[reducible, inline]

abbrev HVector.toPair {α : Type u_3} {A : α → Type u_1} {a₁ : α} {a₂ : α} : HVector A [a₁, a₂] → A a₁ × A a₂

Equations

• HVector.toPair = HVector.toTuple

@[reducible, inline]

abbrev HVector.toTriple {α : Type u_3} {A : α → Type u_1} {a₁ : α} {a₂ : α} {a₃ : α} : HVector A [a₁, a₂, a₃] → A a₁ × A a₂ × A a₃

Equations

• HVector.toTriple = HVector.toTuple

instance HVector.instRepr {α : Type u_3} {as : List α} {f : α → Type u_4} [(a : α) → Repr (f a)] : Repr (HVector f as)

Equations

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

theorem HVector.map_map {α : Type u_6} {A : α → Type u_3} {B : α → Type u_4} {C : α → Type u_5} {l : List α} (t : HVector A l) (f : (a : α) → A a → B a) (g : (a : α) → B a → C a) : HVector.map g (HVector.map f t) = HVector.map (fun (a : α) (v : A a) => g a (f a v)) t

theorem HVector.eq_of_type_eq_nil {α : Type u_4} {A : α → Type u_3} {l : List α} {t₁ : HVector A l} {t₂ : HVector A l} (h : l = []) : t₁ = t₂

def HVector.«term[_]ₕ» : Lean.ParserDescr

Equations

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

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

Equations

• HVector.«term_::ₕ_» = Lean.ParserDescr.trailingNode `HVector.«term_::ₕ_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "::ₕ") (Lean.ParserDescr.cat `term 51))