refl

Mathlib.Computability.TMComputable

URI: https://scilib.ai/kg/mathlib#Turing.EvalsTo.refl

Lean4

/-- Reflexivity of `EvalsTo` in 0 steps. -/
def refl {σ : Type*} (f : σ → Option σ) (a : σ) : EvalsTo f a (some a) :=
  ⟨0, rfl⟩

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

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

Разделы

Аффилиация

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