Skip to content

refactor(MultiTapeTM): Rename TransitionOut to Action and its fields after the tapes - #827

Open
barni120400 wants to merge 1 commit into
leanprover:mainfrom
barni120400:multitape/action-names
Open

refactor(MultiTapeTM): Rename TransitionOut to Action and its fields after the tapes#827
barni120400 wants to merge 1 commit into
leanprover:mainfrom
barni120400:multitape/action-names

Conversation

@barni120400

Copy link
Copy Markdown

Renames TransitionOut to Action, and its fields after the tapes they act on, so that Action.inputTape reads as the action on the input tape and likewise for the others.

TransitionOut Action
inputMove inputTape
workActions workTapes
outS output
q' state

step now projects from the action rather than destructuring its fields, since workTapes and state would otherwise shadow the configuration's fields of the same name. Docstrings updated to match.

NB: claude was used heavily throughout.

…lds after the tapes

Each field now names the tape it acts on, so `Action.inputTape` reads as
the action on the input tape and likewise for the others.

  TransitionOut -> Action    inputMove -> inputTape    outS -> output
                             workActions -> workTapes  q'   -> state

`step` projects from the action instead of destructuring, since
`workTapes` and `state` would otherwise shadow the configuration's fields
of the same name.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@barni120400
barni120400 force-pushed the multitape/action-names branch from aa02129 to 1519cdf Compare August 20, 2026 15:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants