Commit 2025-02-19 18:19 02e69d83

View on Github →

chore: split TMToPartrec.lean (#22068) This is a minimal modification which just separates the material on Code and Cfg as a file TMConfig.lean that is then imported to TMToPartrec.lean.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Computability/TMConfig.lean

added def Turing.ToPartrec.Cfg.then

added inductive Turing.ToPartrec.Cfg

added theorem Turing.ToPartrec.Code.Ok.zero

added def Turing.ToPartrec.Code.Ok

added theorem Turing.ToPartrec.Code.case_eval

added theorem Turing.ToPartrec.Code.comp_eval

added theorem Turing.ToPartrec.Code.cons_eval

added def Turing.ToPartrec.Code.eval

added theorem Turing.ToPartrec.Code.exists_code.comp

added theorem Turing.ToPartrec.Code.exists_code

added theorem Turing.ToPartrec.Code.fix_eval

added def Turing.ToPartrec.Code.head

added theorem Turing.ToPartrec.Code.head_eval

added def Turing.ToPartrec.Code.id

added theorem Turing.ToPartrec.Code.id_eval

added def Turing.ToPartrec.Code.nil

added theorem Turing.ToPartrec.Code.nil_eval

added def Turing.ToPartrec.Code.prec

added def Turing.ToPartrec.Code.pred

added theorem Turing.ToPartrec.Code.pred_eval

added def Turing.ToPartrec.Code.rfind

added theorem Turing.ToPartrec.Code.succ_eval

added theorem Turing.ToPartrec.Code.tail_eval

added theorem Turing.ToPartrec.Code.zero'_eval

added def Turing.ToPartrec.Code.zero

added theorem Turing.ToPartrec.Code.zero_eval

added inductive Turing.ToPartrec.Code

added def Turing.ToPartrec.Cont.eval

added def Turing.ToPartrec.Cont.then

added theorem Turing.ToPartrec.Cont.then_eval

added inductive Turing.ToPartrec.Cont

added theorem Turing.ToPartrec.code_is_ok

added theorem Turing.ToPartrec.cont_eval_fix

added def Turing.ToPartrec.step

added theorem Turing.ToPartrec.stepNormal.is_ret

added def Turing.ToPartrec.stepNormal

added theorem Turing.ToPartrec.stepNormal_eval

added theorem Turing.ToPartrec.stepNormal_then

added def Turing.ToPartrec.stepRet

added theorem Turing.ToPartrec.stepRet_eval

added theorem Turing.ToPartrec.stepRet_then

Modified Mathlib/Computability/TMToPartrec.lean

deleted def Turing.ToPartrec.Cfg.then

deleted inductive Turing.ToPartrec.Cfg

deleted theorem Turing.ToPartrec.Code.Ok.zero

deleted def Turing.ToPartrec.Code.Ok

deleted theorem Turing.ToPartrec.Code.case_eval

deleted theorem Turing.ToPartrec.Code.comp_eval

deleted theorem Turing.ToPartrec.Code.cons_eval

deleted def Turing.ToPartrec.Code.eval

deleted theorem Turing.ToPartrec.Code.exists_code.comp

deleted theorem Turing.ToPartrec.Code.exists_code

deleted theorem Turing.ToPartrec.Code.fix_eval

deleted def Turing.ToPartrec.Code.head

deleted theorem Turing.ToPartrec.Code.head_eval

deleted def Turing.ToPartrec.Code.id

deleted theorem Turing.ToPartrec.Code.id_eval

deleted def Turing.ToPartrec.Code.nil

deleted theorem Turing.ToPartrec.Code.nil_eval

deleted def Turing.ToPartrec.Code.prec

deleted def Turing.ToPartrec.Code.pred

deleted theorem Turing.ToPartrec.Code.pred_eval

deleted def Turing.ToPartrec.Code.rfind

deleted theorem Turing.ToPartrec.Code.succ_eval

deleted theorem Turing.ToPartrec.Code.tail_eval

deleted theorem Turing.ToPartrec.Code.zero'_eval

deleted def Turing.ToPartrec.Code.zero

deleted theorem Turing.ToPartrec.Code.zero_eval

deleted inductive Turing.ToPartrec.Code

deleted def Turing.ToPartrec.Cont.eval

deleted def Turing.ToPartrec.Cont.then

deleted theorem Turing.ToPartrec.Cont.then_eval

deleted inductive Turing.ToPartrec.Cont

deleted theorem Turing.ToPartrec.code_is_ok

deleted theorem Turing.ToPartrec.cont_eval_fix

deleted def Turing.ToPartrec.step

deleted theorem Turing.ToPartrec.stepNormal.is_ret

deleted def Turing.ToPartrec.stepNormal

deleted theorem Turing.ToPartrec.stepNormal_eval

deleted theorem Turing.ToPartrec.stepNormal_then

deleted def Turing.ToPartrec.stepRet

deleted theorem Turing.ToPartrec.stepRet_eval

deleted theorem Turing.ToPartrec.stepRet_then