basic): review comparison API
#14940

Open

feat(set_theory/game/basic): review comparison API #14940

vihdzp wants to merge 6 commits into master from tweak_comp_lemmas_pgame

review comparison API

8d14517b

vihdzp added awaiting-review

vihdzp requested a review from

alreadydone 3 years ago

fix + tweak

f8412ad7

tweak + fix

350f8718

tweak

02e5380c

fix

e2771366

golf

c22e6e4f

alreadydone requested changes on 2022-06-26

vihdzp marked this pull request as draft 3 years ago

vihdzp added WIP

urkud assigned

digama0 3 years ago

kim-em removed awaiting-review

kim-em added too-late

Reviewers

alreadydone

Assignees

digama0

Labels

WIP too-late

Milestone

No milestone