From 41c2d502faa775dcb0a7b75b486c34125be03298 Mon Sep 17 00:00:00 2001
From: Jay Lorch <jaylorch@gmail.com>
Date: Thu, 19 Mar 2026 13:58:10 -0700
Subject: [PATCH] Simplify Number::eq spec

---
 src/number.rs | 48 +++++++++++++++++++++---------------------------
 1 file changed, 21 insertions(+), 27 deletions(-)

diff --git a/src/number.rs b/src/number.rs
index 10392ef..5857c3b 100644
--- a/src/number.rs
+++ b/src/number.rs
@@ -578,33 +578,27 @@ impl PartialEq for Number {
         ensures
             match (self@, other@) {
                 (NumberView::Integer(n1), NumberView::Integer(n2)) => result == (n1 == n2),
-                (NumberView::Float(f1), NumberView::Integer(n2)) => {
-                    ||| float_to_small_int(f1) matches Some(n1) && result == (n1 == n2)
-                    ||| exists|f2: f64| #![trigger other@.to_f64_lossy_ensures(f2)] {
-                        &&& float_to_small_int(f1) is None
-                        &&& other@.to_f64_lossy_ensures(f2)
-                        &&& result == (!f1.is_nan_spec() && !f2.is_nan_spec() && f1.eq_spec(&f2))
-                    }
-                },
-                (NumberView::Integer(n1), NumberView::Float(f2)) => {
-                    ||| float_to_small_int(f2) matches Some(n2) && result == (n1 == n2)
-                    ||| exists|f1: f64| #![trigger self@.to_f64_lossy_ensures(f1)] {
-                        &&& float_to_small_int(f2) is None
-                        &&& self@.to_f64_lossy_ensures(f1)
-                        &&& result == (!f1.is_nan_spec() && !f2.is_nan_spec() && f1.eq_spec(&f2))
-                    }
-                },
-                (NumberView::Float(f1), NumberView::Float(f2)) => {
-                    ||| {
-                        &&& float_to_small_int(f1) matches Some(n1)
-                        &&& float_to_small_int(f2) matches Some(n2)
-                        &&& result == (n1 == n2)
-                    }
-                    ||| {
-                        &&& float_to_small_int(f1) is None || float_to_small_int(f2) is None
-                        &&& result == (!f1.is_nan_spec() && !f2.is_nan_spec() && f1.eq_spec(&f2))
-                    }
-                }
+                (NumberView::Float(f1), NumberView::Integer(n2)) =>
+                    match float_to_small_int(f1) {
+                        Some(n1) => result == (n1 == n2),
+                        None => exists|f2: f64| #![trigger other@.to_f64_lossy_ensures(f2)] {
+                            &&& other@.to_f64_lossy_ensures(f2)
+                            &&& result == (!f1.is_nan_spec() && !f2.is_nan_spec() && f1.eq_spec(&f2))
+                        },
+                    },
+                (NumberView::Integer(n1), NumberView::Float(f2)) =>
+                    match float_to_small_int(f2) {
+                        Some(n2) => result == (n1 == n2),
+                        None => exists|f1: f64| #![trigger self@.to_f64_lossy_ensures(f1)] {
+                            &&& self@.to_f64_lossy_ensures(f1)
+                            &&& result == (!f1.is_nan_spec() && !f2.is_nan_spec() && f1.eq_spec(&f2))
+                        },
+                    },
+                (NumberView::Float(f1), NumberView::Float(f2)) =>
+                    match (float_to_small_int(f1), float_to_small_int(f2)) {
+                        (Some(n1), Some(n2)) => result == (n1 == n2),
+                        _ => result == (!f1.is_nan_spec() && !f2.is_nan_spec() && f1.eq_spec(&f2)),
+                    },
             },
     )]
     fn eq(&self, other: &Self) -> bool {