Commit 2026-02-17 15:39 80378d40
View on Github →refactor(Computability): file for state transition systems (#33291)
This PR makes a new file to contain content having to do with state transition systems defined by a function σ → Option σ. This content was previously split over PostTuringMachine.lean and TMComputable.lean, but since these definitions don't only apply to Turing machines in particular, it seems sensible to refactor them and remove them from the Turing namespace and put them in a new StateTransition namespace.