chore: fix definition case

leanprover · Jan 14, 2025 · c8ed74e · c8ed74e
1 parent 8c3448f
commit c8ed74e
Showing 1 changed file with 7 additions and 5 deletions.
diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
@@ -669,39 +669,41 @@ def ofBoolListLE : (bs : List Bool) → BitVec bs.length
 | [] => 0#0
 | b :: bs => concat (ofBoolListLE bs) b
 
+/-! ## Overflow -/
+
 /-- Overflow predicate for 2's complement unary minus.
 
   SMT-Lib name: `bvnego`.
 -/
 
-def not_overflow {w : Nat} (x : BitVec w) : Bool := x.toInt == - (2 ^ (w - 1))
+def notOverflow {w : Nat} (x : BitVec w) : Bool := x.toInt == - (2 ^ (w - 1))
 
 /-- Overflow predicate for unsigned addition modulo 2^w.
 
   SMT-Lib name: `bvuaddo`.
 -/
 
-def uadd_overflow {w : Nat} (x y : BitVec w) : Bool := x.toNat + y.toNat ≥ 2 ^ w
+def uaddOverflow {w : Nat} (x y : BitVec w) : Bool := x.toNat + y.toNat ≥ 2 ^ w
 
 /-- Overflow predicate for signed addition on w-bit 2's complement.
 
   SMT-Lib name: `bvsaddo`.
 -/
 
-def sadd_overflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt + y.toInt ≥ 2 ^ (w - 1)) || (x.toInt + y.toInt < - 2 ^ (w - 1))
+def saddOverflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt + y.toInt ≥ 2 ^ (w - 1)) || (x.toInt + y.toInt < - 2 ^ (w - 1))
 
 /-- Overflow predicate for unsigned multiplication modulo 2^w.
 
   SMT-Lib name: `bvumulo`.
 -/
 
-def umul_overflow {w : Nat} (x y : BitVec w) : Bool := x.toNat * y.toNat ≥ 2 ^ w
+def umulOverflow {w : Nat} (x y : BitVec w) : Bool := x.toNat * y.toNat ≥ 2 ^ w
 
 /-- Overflow predicate for signed multiplication on w-bit 2's complement.
 
   SMT-Lib name: `bvsmulo`.
 -/
 
-def smul_overflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt * y.toInt ≥ 2 ^ (w - 1)) || (x.toInt * y.toInt < - 2 ^ (w - 1))
+def smulOverflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt * y.toInt ≥ 2 ^ (w - 1)) || (x.toInt * y.toInt < - 2 ^ (w - 1))
 
 end BitVec