Google Git Google Git
Sign in
fuchsia/third_party/github.com/leanprover/lean4/refs/heads/upstream/expose-array-back/./tests/elab/floatEquality.lean
blob: b2d00a1ba5784aa281e67f0cede19ba8c299b037 [file] [edit]
/-!
Tests for the `DecidableEq Float` and `BEq Float` instances
-/
/-- info: false -/
#guard_msgs in
#eval 0.1 == 0.2
/-- info: true -/
#guard_msgs in
#eval 0.1 == 0.1
/-- info: true -/
#guard_msgs in
#eval 0.1 == 0.100000000000000001
/-- info: true -/
#guard_msgs in
#eval 0.0 == -0.0
/-- info: false -/
#guard_msgs in
#eval (0.0 / 0.0) == (0.0 / 0.0)
/-- info: false -/
#guard_msgs in
#eval 0.1 = 0.2
/-- info: true -/
#guard_msgs in
#eval 0.1 = 0.1
/-- info: true -/
#guard_msgs in
#eval 0.1 = 0.100000000000000001
/-- info: false -/
#guard_msgs in
#eval 0.0 = -0.0
/-- info: true -/
#guard_msgs in
#eval (0.0 / 0.0) = (0.0 / 0.0)