def Vect (n : Nat) (A : Sort u) : Sort u

Equations

• Vect n A = (Fin n → A)

def Vect.nil {A : Sort u_1} : Vect 0 A

def Vect.cons {A : Sort u_1} {n : Nat} (head : A) (tail : Vect n A) : Vect (n + 1) A

Equations

• head :: tail = Fin.cases head tail

def vect_cons : Lean.TrailingParserDescr

Equations

• vect_cons = Lean.ParserDescr.trailingNode `vect_cons 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " :: ") (Lean.ParserDescr.cat `term 67))

@[simp]

theorem Vect.cons_zero {n : Nat} {A : Sort u_1} {hd : A} {tl : Vect n A} : (hd :: tl) 0 = hd

@[simp]

theorem Vect.cons_succ {n : Nat} {A : Sort u_1} {hd : A} {i : Fin n} {tl : Vect n A} : (hd :: tl) i.succ = tl i

@[simp]

theorem Vect.eta0 {A : Sort u_1} {v : Vect 0 A} : v = nil

def Vect.head {n : Nat} {A : Sort u_1} (v : Vect (n + 1) A) : A

Equations

• v.head = v 0

@[simp]

theorem Vect.head_cons {A✝ : Sort u_1} {hd : A✝} {n✝ : Nat} {tl : Vect n✝ A✝} : (hd :: tl).head = hd

def Vect.tail {n : Nat} {A : Sort u_1} (v : Vect (n + 1) A) : Vect n A

Equations

• v.tail x✝ = v x✝.succ

@[simp]

theorem Vect.tail_cons {A✝ : Sort u_1} {hd : A✝} {n✝ : Nat} {tl : Vect n✝ A✝} : (hd :: tl).tail = tl

def Vect.uncons {n : Nat} {A : Sort u_1} (v : Vect (n + 1) A) : A ×' Vect n A

Equations

• v.uncons = ⟨v.head, v.tail⟩

@[simp]

theorem Vect.uncons_cons {A✝ : Sort u_1} {hd : A✝} {n✝ : Nat} {tl : Vect n✝ A✝} : (hd :: tl).uncons = ⟨hd, tl⟩

theorem Vect.uncons_iff {a✝ : Nat} {A✝ : Sort u_1} {v : Vect (a✝ + 1) A✝} {hd : A✝} {tl : Vect a✝ A✝} : v.uncons = ⟨hd, tl⟩ ↔ v = hd :: tl

def Vect.induction {motive : (n : Nat) → (A : Sort u1) → Vect n A → Sort u2} {A : Sort u1} (nil : motive 0 A nil) (cons : {n : Nat} → {tl : Vect n A} → (hd : A) → motive n A tl → motive (n + 1) A (hd :: tl)) {n : Nat} (v : Vect n A) : motive n A v

Equations

• One or more equations did not get rendered due to their size.
• Vect.induction nil cons v = ⋯.mpr nil

@[simp]

theorem Vect.induction_nil {motive✝ : (n : Nat) → (A : Sort u_1) → Vect n A → Sort u_2} {A✝ : Sort u_1} {ni : motive✝ 0 A✝ nil} {co : {n : Nat} → {tl : Vect n A✝} → (hd : A✝) → motive✝ n A✝ tl → motive✝ (n + 1) A✝ (hd :: tl)} : induction ni co nil = ni

@[simp]

theorem Vect.induction_cons {motive✝ : (n : Nat) → (A : Sort u_1) → Vect n A → Sort u_2} {A✝ : Sort u_1} {ni : motive✝ 0 A✝ nil} {co : {n : Nat} → {tl : Vect n A✝} → (hd : A✝) → motive✝ n A✝ tl → motive✝ (n + 1) A✝ (hd :: tl)} {hd : A✝} {n✝ : Nat} {tl : Vect n✝ A✝} : induction ni co (hd :: tl) = co hd (induction ni (fun {n : Nat} {tl : Vect n A✝} => co) tl)

def Vect.fold {B : Sort u_1} {A : Sort u1} (d : B) (f : A → B → B) {n : Nat} (v : Vect n A) : B

Equations

• Vect.fold d f v = Vect.induction d (fun {n : Nat} {tl : Vect n A} => f) v

@[simp]

theorem Vect.fold_nil {α✝ : Sort u_1} {d : α✝} {A✝ : Sort u_2} {f : A✝ → α✝ → α✝} : fold d f nil = d

@[simp]

theorem Vect.fold_cons {α✝ : Sort u_1} {d : α✝} {A✝ : Sort u_2} {f : A✝ → α✝ → α✝} {hd : A✝} {n✝ : Nat} {tl : Vect n✝ A✝} : fold d f (hd :: tl) = f hd (fold d f tl)

@[simp]

theorem Vect.map_id {n : Nat} {A : Sort u_1} {v : Vect n A} : (fun (n : Fin n) => id (v n)) = v

theorem Vect.map_compose {n : Nat} {A : Sort u_1} {β✝ : Sort u_2} {δ✝ : Sort u_3} {f : β✝ → δ✝} {g : A → β✝} {v : Vect n A} : (fun (n_1 : Fin n) => f ((fun (n : Fin n) => g (v n)) n_1)) = fun (n : Fin n) => (f ∘ g) (v n)