Commit 2023-04-18 03:36 bb3869b8

View on Github →

feat: port Computability.TMComputable (#2800)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Computability/TMComputable.lean

added def Turing.EvalsTo.refl

added def Turing.EvalsTo.trans

added structure Turing.EvalsTo

added def Turing.EvalsToInTime.refl

added def Turing.EvalsToInTime.trans

added structure Turing.EvalsToInTime

added def Turing.FinTM2.Cfg

added def Turing.FinTM2.Stmt

added def Turing.FinTM2.step

added structure Turing.FinTM2

added structure Turing.TM2Computable

added structure Turing.TM2ComputableAux

added def Turing.TM2ComputableInPolyTime.toTM2ComputableInTime

added structure Turing.TM2ComputableInPolyTime

added def Turing.TM2ComputableInTime.toTM2Computable

added structure Turing.TM2ComputableInTime

added def Turing.TM2Outputs

added def Turing.TM2OutputsInTime.toTM2Outputs

added def Turing.TM2OutputsInTime

added def Turing.haltList

added def Turing.idComputable

added def Turing.idComputableInPolyTime

added def Turing.idComputableInTime

added def Turing.idComputer

added def Turing.initList