Theorems · Definition · combinatorics

List.Vector.casesOn

{α : Type u_1} →
  {m : ℕ} →
    {motive : {n : ℕ} → List.Vector α n → Sort u_8} →
      (v : List.Vector α m) →
        motive List.Vector.nil → ({n : ℕ} → (hd : α) → (tl : List.Vector α n) → motive (hd ::ᵥ tl)) → motive v

Define motive v by case-analysis on v : Vector α n.

Defined in

Mathlib.Data.Vector.Basic

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext