nnreal): make `real.to_nnreal` computable
#16645

Open

chore(data/real/nnreal): make `real.to_nnreal` computable #16645

eric-wieser wants to merge 3 commits into master from eric-wieser/computable-to_real

chore(data/real/nnreal): make `real.to_nnreal` computable

75cfb661

eric-wieser force pushed from fa6d0bcd to 75cfb661 3 years ago

mathlib-dependent-issues-bot added blocked-by-other-PR

eric-wieser removed blocked-by-other-PR

eric-wieser added easy

eric-wieser added awaiting-review

eric-wieser removed easy

eric-wieser requested a review from

YaelDillies 3 years ago

mathlib-dependent-issues-bot added blocked-by-other-PR

YaelDillies approved these changes on 2022-09-26

mathlib-dependent-issues-bot removed blocked-by-other-PR

fix noisiness

010e590c

485ec7ec

kim-em added too-late

Reviewers

YaelDillies

Assignees

No one assigned

Labels

awaiting-review too-late

Milestone

No milestone