Theorems · Theorem · combinatorics

List.Vector.inductionOn_nil

∀ {α : Type u_1} {C : {n : ℕ} → List.Vector α n → Sort u_6} (nil : C List.Vector.nil)
  (cons : {n : ℕ} → {x : α} → {w : List.Vector α n} → C w → C (x ::ᵥ w)),
  (List.Vector.nil.inductionOn nil fun {n} {x} {w} => cons) = nil

Defined in

Mathlib.Data.Vector.Basic

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext