max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: note that Float.beq is not refl

Browse source
This commit is contained in:
E.W.Ayers 2022-08-12 11:03:56 +01:00 • committed by Leonardo de Moura
parent 969dce70db
commit 152d441a4c
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Init/Data/Float.lean
View file

@ -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⟩