Commit 2025-01-16 21:58 fc139ddc

View on Github →

chore(Mathlib/Computability/TuringMachine): split file (#20790) This PR splits Mathlib/Computability/TuringMachine by moving to a new file the initial 600 or so lines, which deal with the definition of the tape data structure that a Turing machine uses. This reduces the size of this large file to less than 2100 lines.

Estimated changes

added theorem Turing.BlankRel.refl
added theorem Turing.BlankRel.symm
added theorem Turing.BlankRel.trans
added def Turing.BlankRel
added inductive Turing.Dir
added theorem Turing.ListBlank.ext
added def Turing.ListBlank
added structure Turing.PointedMap.{u,
added theorem Turing.Tape.exists_mk'
added def Turing.Tape.map
added theorem Turing.Tape.map_fst
added theorem Turing.Tape.map_mk'
added theorem Turing.Tape.map_mk₁
added theorem Turing.Tape.map_mk₂
added theorem Turing.Tape.map_move
added theorem Turing.Tape.map_write
added def Turing.Tape.mk'
added theorem Turing.Tape.mk'_head
added theorem Turing.Tape.mk'_left
added theorem Turing.Tape.mk'_right
added def Turing.Tape.move
added def Turing.Tape.nth
added theorem Turing.Tape.nth_zero
added theorem Turing.Tape.write_mk'
added theorem Turing.Tape.write_nth
added theorem Turing.Tape.write_self
added structure Turing.Tape
added def Turing.proj
added theorem Turing.proj_map_nth
deleted theorem Turing.BlankExtends.refl
deleted theorem Turing.BlankExtends.trans
deleted def Turing.BlankExtends
deleted theorem Turing.BlankRel.refl
deleted theorem Turing.BlankRel.symm
deleted theorem Turing.BlankRel.trans
deleted def Turing.BlankRel
deleted inductive Turing.Dir
deleted theorem Turing.ListBlank.cons_mk
deleted theorem Turing.ListBlank.ext
deleted theorem Turing.ListBlank.head_map
deleted theorem Turing.ListBlank.head_mk
deleted theorem Turing.ListBlank.map_cons
deleted theorem Turing.ListBlank.map_mk
deleted def Turing.ListBlank.mk
deleted theorem Turing.ListBlank.nth_map
deleted theorem Turing.ListBlank.nth_mk
deleted theorem Turing.ListBlank.nth_succ
deleted theorem Turing.ListBlank.nth_zero
deleted theorem Turing.ListBlank.tail_map
deleted theorem Turing.ListBlank.tail_mk
deleted def Turing.ListBlank
deleted theorem Turing.PointedMap.map_pt
deleted theorem Turing.PointedMap.mk_val
deleted structure Turing.PointedMap.{u,
deleted theorem Turing.Tape.exists_mk'
deleted def Turing.Tape.left₀
deleted def Turing.Tape.map
deleted theorem Turing.Tape.map_fst
deleted theorem Turing.Tape.map_mk'
deleted theorem Turing.Tape.map_mk₁
deleted theorem Turing.Tape.map_mk₂
deleted theorem Turing.Tape.map_move
deleted theorem Turing.Tape.map_write
deleted def Turing.Tape.mk'
deleted theorem Turing.Tape.mk'_head
deleted theorem Turing.Tape.mk'_left
deleted theorem Turing.Tape.mk'_nth_nat
deleted theorem Turing.Tape.mk'_right
deleted theorem Turing.Tape.mk'_right₀
deleted def Turing.Tape.mk₁
deleted def Turing.Tape.mk₂
deleted def Turing.Tape.move
deleted theorem Turing.Tape.move_left_mk'
deleted theorem Turing.Tape.move_left_nth
deleted def Turing.Tape.nth
deleted theorem Turing.Tape.nth_zero
deleted theorem Turing.Tape.right₀_nth
deleted def Turing.Tape.write
deleted theorem Turing.Tape.write_mk'
deleted theorem Turing.Tape.write_nth
deleted theorem Turing.Tape.write_self
deleted structure Turing.Tape
deleted def Turing.proj
deleted theorem Turing.proj_map_nth