mathlib3

282da0c1 - feat(set_theory/game/nim): make the file `noncomputable theory` (#15367)

feat(set_theory/game/nim): make the file `noncomputable theory` (#15367) Since we're interfacing with ordinals and since `pgame` holds no data, we simplify `nim` and allow it to be noncomputable. We need to give `nim` the `noncomputable!` attribute to avoid a VM compilation bug.