Commit 2025-02-05 05:32 61e40897

View on Github →

chore: cleanup porting notes in TuringMachine (#20821) Many local notations were added during porting. To my eye, they don't improve readability at all, but if others disagree we can do something else. However, if you don't like this PR, please either resolve the porting notes alternately, or at least let me know how you would like it done (possibly just deleting them).

Estimated changes

modified def Turing.TM0.Reaches
modified def Turing.TM0.Supports
modified def Turing.TM0.eval
modified def Turing.TM0.init
modified def Turing.TM0.step
modified theorem Turing.TM0.step_supports
modified theorem Turing.TM0.univ_supports
modified def Turing.TM0to1.tr
modified def Turing.TM0to1.trCfg
modified def Turing.TM1.Supports
modified def Turing.TM1.eval
modified def Turing.TM1.init
modified def Turing.TM1.step
modified def Turing.TM1.stepAux
modified theorem Turing.TM1.step_supports
modified theorem Turing.TM1.stmts_trans
modified theorem Turing.TM1.stmts₁_self
modified theorem Turing.TM1.stmts₁_trans
modified def Turing.TM1to0.tr
modified def Turing.TM1to0.trAux
modified def Turing.TM1to0.trCfg
modified def Turing.TM1to1.move
modified def Turing.TM1to1.read
modified def Turing.TM1to1.readAux
modified theorem Turing.TM1to1.stepAux_move
modified theorem Turing.TM1to1.stepAux_read
modified theorem Turing.TM1to1.stepAux_write
modified def Turing.TM1to1.tr
modified def Turing.TM1to1.trCfg
modified def Turing.TM1to1.write
modified def Turing.TM2.Reaches
modified def Turing.TM2.Supports
modified def Turing.TM2.eval
modified def Turing.TM2.init
modified def Turing.TM2.step
modified def Turing.TM2.stepAux
modified theorem Turing.TM2.step_supports
modified theorem Turing.TM2.stmts_trans
modified theorem Turing.TM2.stmts₁_self
modified theorem Turing.TM2.stmts₁_trans
modified inductive Turing.TM2to1.TrCfg
modified def Turing.TM2to1.stRun
modified def Turing.TM2to1.stVar
modified def Turing.TM2to1.stWrite
modified theorem Turing.TM2to1.step_run
modified theorem Turing.TM2to1.supports_run
modified def Turing.TM2to1.tr
modified theorem Turing.TM2to1.trCfg_init
modified def Turing.TM2to1.trInit
modified theorem Turing.TM2to1.trNormal_run
modified def Turing.TM2to1.trStAct