move_right_mk' — Mathlib

English

Moving right on Tape.mk' L R yields Tape.mk' (L.cons R.head) R.tail.

Русский

Перемещение вправо относительно Tape.mk' L R даёт Tape.mk' (L.cons R.head) R.tail.

LaTeX

$$$\forall {\Gamma} [Inhabited(\Gamma)] (L R : ListBlank(\Gamma)), (Tape.move\ Dir.right\ (Tape.mk' L R)) = Tape.mk' (L.cons R.head) R.tail$$$

Lean4

@[simp]
theorem move_right_mk' {Γ} [Inhabited Γ] (L R : ListBlank Γ) :
    (Tape.mk' L R).move Dir.right = Tape.mk' (L.cons R.head) R.tail := by simp only [Tape.move, Tape.mk']

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