Mathlib v3 is deprecated. Go to Mathlib v4

Inductive relation.game_add

Modification history

2022-08-16 10:36
src/logic/hydra.lean
refactor(order/game_add): move `game_add` to its own file (#15885) …
Deleted relation.game_addView on Github →
2022-05-23 01:49
src/logic/hydra.lean
feat(logic/hydra): termination of a hydra game (#14190) …
Added relation.game_addView on Github →