Commit 2024-08-09 12:27 74b685eb

View on Github →

fix: variables in TuringMachine.lean (#15422) This is work by @digama0 that I'm backport from the lean-pr-testing-4814 branch.

Estimated changes

modified structure Turing.TM0.Cfg
modified def Turing.TM0.Reaches
modified def Turing.TM0.init
modified structure Turing.TM1.Cfg
modified def Turing.TM1.step
modified def Turing.TM1.stepAux
modified def Turing.TM1to0.trCfg
modified theorem Turing.TM1to0.tr_eval
modified theorem Turing.TM1to0.tr_respects
modified theorem Turing.TM1to1.tr_supports