Theorems · Definition · combinatorics

List.Vector.inductionOn

{α : Type u_1} →
  {C : {n : ℕ} → List.Vector α n → Sort u_6} →
    {n : ℕ} →
      (v : List.Vector α n) → C List.Vector.nil → ({n : ℕ} → {x : α} → {w : List.Vector α n} → C w → C (x ::ᵥ w)) → C v

Define C v by induction on v : Vector α n. This function has two arguments: nil handles the base case on C nil, and cons defines the inductive step using ∀ x : α, C w → C (x ::ᵥ w). It is used as the default induction principle for the induction tactic.

Defined in

Mathlib.Data.Vector.Basic

Cited by

10 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext