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: May 02 2025 at 03:31 UTC