Zulip Chat Archive
Stream: mathlib4
Topic: Coercion from NNReal to ENNReal
Yury G. Kudryashov (Feb 18 2023 at 23:01):
Should I use docs4#WithTop.cast or define a new function?
Yury G. Kudryashov (Feb 19 2023 at 01:06):
I defined NNReal.toENNReal because ENNReal dot notation doesn't work with WithTop.some x
Last updated: Dec 20 2023 at 11:08 UTC