From 152d441a4ca94b984bb7e1e3517950bb5fcd86f8 Mon Sep 17 00:00:00 2001 From: "E.W.Ayers" Date: Fri, 12 Aug 2022 11:03:56 +0100 Subject: [PATCH] doc: note that Float.beq is not refl --- src/Init/Data/Float.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean index 75f2285498..ee44c8ec53 100644 --- a/src/Init/Data/Float.lean +++ b/src/Init/Data/Float.lean @@ -53,6 +53,7 @@ instance : Neg Float := ⟨Float.neg⟩ instance : LT Float := ⟨Float.lt⟩ instance : LE Float := ⟨Float.le⟩ +/-- Note: this is not reflexive since `NaN != NaN`.-/ @[extern "lean_float_beq"] opaque Float.beq (a b : Float) : Bool instance : BEq Float := ⟨Float.beq⟩