recOn

Mathlib.Data.Seq.Defs

URI: https://scilib.ai/kg/mathlib#Stream'.Seq.recOn

Lean4

/-- Recursion principle for sequences, compare with `List.recOn`. -/
@[cases_eliminator]
def recOn {motive : Seq α → Sort v} (s : Seq α) (nil : motive nil) (cons : ∀ x s, motive (cons x s)) : motive s :=
  by
  rcases H : destruct s with - | v
  · rw [destruct_eq_none H]
    apply nil
  · obtain ⟨a, s'⟩ := v
    rw [destruct_eq_cons H]
    apply cons

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru