Commit 2026-03-10 01:33 374f54cf

chore(Computability): move TM files to a single folder (#35608) This PR takes files relevant to Turing machines and moves them to a single folder for better organization. In the process, we do some renaming of these files

• We remove the "TM" from the front of these files, as it's now redundant.
• TuringMachine.lean --> TuringMachine/StackTuringMachine.lean
  • (really the key difference between the TM2 model presented in this file, and the TM1 model from the previous, is the introduction of stacks instead of tapes) I also remove EvalsTo and friends from TuringMachine.Computable, as these in #33291 were moved out of the TM namespace. https://github.com/leanprover-community/mathlib4/pull/35609 is a follow-up PR to add module deprecations.