From 854ab51de12b08210d8a83fcc7b752c0a3341f73 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 21 Feb 2024 23:48:42 +0000 Subject: [PATCH] =?UTF-8?q?chore:=20`pp=5Fdot`=20on=20`=E2=84=9D=E2=89=A50?= =?UTF-8?q?=E2=88=9E`=20definitions=20(#10837)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Data/ENNReal/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/ENNReal/Basic.lean b/Mathlib/Data/ENNReal/Basic.lean index 3d70e7926194b..2554868a0e142 100644 --- a/Mathlib/Data/ENNReal/Basic.lean +++ b/Mathlib/Data/ENNReal/Basic.lean @@ -187,11 +187,11 @@ theorem range_coe' : range ofNNReal = Iio ∞ := WithTop.range_coe theorem range_coe : range ofNNReal = {∞}ᶜ := (isCompl_range_some_none ℝ≥0).symm.compl_eq.symm /-- `toNNReal x` returns `x` if it is real, otherwise 0. -/ -protected def toNNReal : ℝ≥0∞ → ℝ≥0 := WithTop.untop' 0 +@[pp_dot] protected def toNNReal : ℝ≥0∞ → ℝ≥0 := WithTop.untop' 0 #align ennreal.to_nnreal ENNReal.toNNReal /-- `toReal x` returns `x` if it is real, `0` otherwise. -/ -protected def toReal (a : ℝ≥0∞) : Real := a.toNNReal +@[pp_dot] protected def toReal (a : ℝ≥0∞) : Real := a.toNNReal #align ennreal.to_real ENNReal.toReal /-- `ofReal x` returns `x` if it is nonnegative, `0` otherwise. -/