readAux — Mathlib

English

Analogous to readAux in TM1to1 capturing the traversal.

Русский

Аналогично readAux в TM1to1 для описания обхода.

LaTeX

$$readAuxAnalog$$

Lean4

/-- Read a vector of length `n` from the tape. -/
def readAux : ∀ n, (List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ) → Stmt Bool (Λ' Γ Λ σ) σ
  | 0, f => f Vector.nil
  | i + 1, f =>
    Stmt.branch (fun a _ ↦ a) (Stmt.move Dir.right <| readAux i fun v ↦ f (true ::ᵥ v))
      (Stmt.move Dir.right <| readAux i fun v ↦ f (false ::ᵥ v))

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