memRecOn

Mathlib.Data.Seq.Computation

URI: https://scilib.ai/kg/mathlib#Computation.memRecOn

Lean4

/-- Recursor based on membership -/
def memRecOn {C : Computation α → Sort v} {a s} (M : a ∈ s) (h1 : C (pure a)) (h2 : ∀ s, C s → C (think s)) : C s :=
  by
  haveI T := terminates_of_mem M
  rw [eq_thinkN' s, get_eq_of_mem s M]
  generalize length s = n
  induction n with
  | zero => exact h1
  | succ n IH => exact h2 _ IH

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

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

Разделы

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

Аффилиация

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