step

Mathlib.Computability.TMConfig

URI: https://scilib.ai/kg/mathlib#Turing.ToPartrec.step

Lean4

/-- If we are not done (in `Cfg.halt` state), then we must be still stuck on a continuation, so
this main loop calls `stepRet` with the new continuation. The overall `step` function transitions
from one `Cfg` to another, only halting at the `Cfg.halt` state. -/
def step : Cfg → Option Cfg
  | Cfg.halt _ => none
  | Cfg.ret k v => some (stepRet k v)

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

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

Разделы

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

Аффилиация

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