Commit 2020-05-09 20:30 08d43163

refactor(computability/turing_machine): add list_blank (#2605) This ended up being a major refactor of computability.turing_machine. It started as a change of the definition of turing machine so that the tape is a quotient of lists up to the relation "ends with blanks", but the file is quite old and I updated it to pass the linter as well. I'm not up to speed on the new documentation requirements, but now is a good time to request them for this file. This doesn't add many new theorems, it's mostly just fixes to make it compile again after the change. (Some of the turing machine constructions are also simplified.)