Commit 2026-02-26 13:42 10f17828

View on Github →

refactor(Computability/TMComputable): generalize from FinEncoding (#34779) Much of TMComputable.lean is stated in terms of FinEncoding when only the encode function is used. This PR generalizes statements in TMComputable.lean to take in just the encode function, making them easier to use (since one does not have to additionally provide a decode function and a proof of decode_encode).

Estimated changes

Modified Mathlib/Computability/TMComputable.lean

modified structure Turing.TM2Computable

modified def Turing.TM2ComputableInPolyTime.toTM2ComputableInTime

modified structure Turing.TM2ComputableInPolyTime

modified def Turing.TM2ComputableInTime.toTM2Computable

modified structure Turing.TM2ComputableInTime

modified def Turing.idComputable

modified def Turing.idComputableInPolyTime

modified def Turing.idComputableInTime

modified def Turing.idComputer