read — Mathlib

English

Read reads a symbol via readAux and then moves left to restore position.

Русский

Чтение считывает символ через readAux и затем возвращает позицию влево.

LaTeX

$$read (f) := readAux n (λ v, move n left ∘ f ∘ dec)$$

Lean4

/-- To read a symbol from the tape, we use `readAux` to traverse the symbol,
then return to the original position with `n` moves to the left. -/
def read (f : Γ → Stmt Bool (Λ' Γ Λ σ) σ) : Stmt Bool (Λ' Γ Λ σ) σ :=
  readAux n fun v ↦ move n Dir.left <| f (dec v)

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