Skip to content

Commit 58759d1

Browse files
committed
Fixing ordering to lexicographical
Thanks to @zoep for the idea!
1 parent fa16a9e commit 58759d1

File tree

1 file changed

+8
-8
lines changed

1 file changed

+8
-8
lines changed

src/EVM/Types.hs

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -490,16 +490,16 @@ instance Ord Prop where
490490
PBool a <= PBool b = a <= b
491491
PEq (a :: Expr x) (b :: Expr x) <= PEq (c :: Expr y) (d :: Expr y)
492492
= case eqT @x @y of
493-
Just Refl -> a < c || b < d || (a == c && b == d)
493+
Just Refl -> a <= c || (a == c && b <= d)
494494
Nothing -> toNum a <= toNum c
495-
PLT a b <= PLT c d = a < c || b < d || (a == c && b == d)
496-
PGT a b <= PGT c d = a < c || b < d || (a == c && b == d)
497-
PGEq a b <= PGEq c d = a < c || b < d || (a == c && b == d)
498-
PLEq a b <= PLEq c d = a < c || b < d || (a == c && b == d)
499495
PNeg a <= PNeg b = a <= b
500-
PAnd a b <= PAnd c d = a < c || b < d || (a == c && b == d)
501-
POr a b <= POr c d = a < c || b < d || (a == c && b == d)
502-
PImpl a b <= PImpl c d = a < c || b < d || (a == c && b == d)
496+
PLT a b <= PLT c d = a <= c || (a == c && b <= d)
497+
PGT a b <= PGT c d = a <= c || (a == c && b <= d)
498+
PGEq a b <= PGEq c d = a <= c || (a == c && b <= d)
499+
PLEq a b <= PLEq c d = a <= c || (a == c && b <= d)
500+
PAnd a b <= PAnd c d = a <= c || (a == c && b <= d)
501+
POr a b <= POr c d = a <= c || (a == c && b <= d)
502+
PImpl a b <= PImpl c d = a <= c || (a == c && b <= d)
503503
a <= b = asNum a <= asNum b
504504
where
505505
asNum :: Prop -> Int

0 commit comments

Comments
 (0)