Skip to content

chore: leftMovesmoves_left and rightMovesmoves_right - #391

Open
vihdzp wants to merge 4 commits into
masterfrom
leftMoves
Open

chore: leftMovesmoves_left and rightMovesmoves_right#391
vihdzp wants to merge 4 commits into
masterfrom
leftMoves

Conversation

@vihdzp

@vihdzp vihdzp commented Mar 18, 2026

Copy link
Copy Markdown
Owner

The old names are a holdover from before #195. This PR is largely a find+replace job, so it might be worth double checking!

@vihdzp vihdzp added the t-game This is mainly about combinatorial games label Mar 18, 2026
Comment thread CombinatorialGames/Game/Ordinal.lean Outdated
Comment thread CombinatorialGames/Surreal/Multiplication.lean Outdated
Comment thread CombinatorialGames/Surreal/Pow.lean Outdated
Comment thread CombinatorialGames/Surreal/Real.lean Outdated
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

t-game This is mainly about combinatorial games

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants