write

Mathlib.Computability.Tape

URI: https://scilib.ai/kg/mathlib#Turing.Tape.write

Lean4

/-- Replace the current value of the head on the tape. -/
def write {Γ} [Inhabited Γ] (b : Γ) (T : Tape Γ) : Tape Γ :=
  { T with head := b }

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

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

Разделы

Аффилиация

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