def Lilac.Fun.Vec (A : Sort u) (n : Nat) : Sort u

Equations

• Lilac.Fun.Vec A n = (Fin n → A)

def Lilac.Fun.Vec.nil {A : Sort u_1} : Vec A 0

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

Equations

• Lilac.Fun.Vec.cons head tail = Fin.cases head tail

theorem Lilac.Fun.Vec.cons_zero {A : Sort u_1} {n : Nat} {hd : A} {tl : Vec A n} : cons hd tl 0 = hd

theorem Lilac.Fun.Vec.cons_succ {A : Sort u_1} {n : Nat} {hd : A} {i : Fin n} {tl : Vec A n} : cons hd tl i.succ = tl i

theorem Lilac.Fun.Vec.eta0 {A : Sort u_1} {v : Vec A 0} : v = nil

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

Equations

• v.head = v 0

theorem Lilac.Fun.Vec.head_cons {A✝ : Sort u_1} {hd : A✝} {n✝ : Nat} {tl : Vec A✝ n✝} : (cons hd tl).head = hd

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

Equations

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

theorem Lilac.Fun.Vec.tail_cons {A✝ : Sort u_1} {hd : A✝} {n✝ : Nat} {tl : Vec A✝ n✝} : (cons hd tl).tail = tl

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

Equations

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

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

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lilac.Fun.Vec.induction nil cons v = cast ⋯ nil

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

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

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

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