Theorems · Definition · logic and foundations

List.reverseRec

{α : Type u_1} →
  {motive : List α → Sort u_2} →
    motive [] → ((l : List α) → (a : α) → motive l → motive (l ++ [a])) → (l : List α) → motive l

Induction principle from the right for lists: if a property holds for the empty list, and for l ++ [a] if it holds for l, then it holds for all lists. The principle is given for a Sort-valued predicate, i.e., it can also be used to construct data.

Defined in

Mathlib.Data.List.Induction

Cited by

5 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext