[Merged by Bors] - doc(order/game_add): improve docstrings #18269
Conversation
vihdzp
added
easy
vihdzp
added
the
modifies-synchronized-file
src/order/game_add.lean
Outdated
| It is so called, as it models game addition within combinatorial game theory. If `rα a₁ a₂` means | ||
| that `a₁ ⟶ a₂` is a valid move in game `α`, and `rβ b₁ b₂` means that `b₁ ⟶ b₂` is a valid move |
There was a problem hiding this comment.
This is counterintuitive, because in mathlib we use < rather than >. In terms of games, a₁ < a₂ means a₁ is simpler than a₂, and pgame.subsequent and pgame.is_option have argument orders consistent with this. So it would be better to keep the original order, saying rα a₁ a₂ means that a₂ ⟶ a₁ is a valid move. (You might restore the original notation a and a' if you want.)
There was a problem hiding this comment.
I didn't change the order, this was just a docstring typo. Also, will add the placeholder PR shortly.
There was a problem hiding this comment.
Sorry, what was the typo? And why do you say you didn't change it? pgame.is_option a' a means there's a valid move from a to a', not the other way around, right? So after your modification, the docstring makes wrong sense when applied to rα := pgame.is_option.
There was a problem hiding this comment.
I didn't redefine the function, just renamed variables in an attempt to match is_option and such, then accidentally swapped variables in the docstring.
There was a problem hiding this comment.
Yeah, my comment is on the docstring from the start. Looks good now, thanks!
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
leanprover-community-bot-assistant
added
ready-to-merge
We add simpler descriptions for `game_add` and `well_founded.prod_game_add`, without removing previous references to combinatorial games. Mathlib 4 pair: leanprover-community/mathlib4#1798
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Mathlib 3 pair: leanprover-community/mathlib#18269
Mathlib 3 pair: leanprover-community/mathlib#18269
We add simpler descriptions for
game_addandwell_founded.prod_game_add, without removing previous references to combinatorial games.Mathlib 4 pair: leanprover-community/mathlib4#1798