Theorems · Definition · combinatorics

List.Vector.revInductionOn

{α : Type u_1} →
  {C : {n : ℕ} → List.Vector α n → Sort u_5} →
    {n : ℕ} →
      (v : List.Vector α n) →
        C List.Vector.nil → ({n : ℕ} → (xs : List.Vector α n) → (x : α) → C xs → C (xs.snoc x)) → C v

Define C v by reverse induction on v : Vector α n. That is, break the vector down starting from the right-most element, using snoc This function has two arguments: nil handles the base case on C nil, and snoc defines the inductive step using ∀ x : α, C xs → C (xs.snoc x). This can be used as induction v using Vector.revInductionOn.

Defined in

Mathlib.Data.Vector.Snoc

Cited by

6 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext