chore: add smtlib names in docstrings

opencompl · Jan 13, 2025 · 8c64c87 · 8c64c87
1 parent 8e26dee
commit 8c64c87
Showing 1 changed file with 20 additions and 5 deletions.
diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
@@ -669,23 +669,38 @@ def ofBoolListLE : (bs : List Bool) → BitVec bs.length
 | [] => 0#0
 | b :: bs => concat (ofBoolListLE bs) b
 
-/-- Overflow predicate for 2's complement unary minus -/
+/-- 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))
 
-/-- Overflow predicate for unsigned addition modulo 2^m -/
+/-- Overflow predicate for unsigned addition modulo 2^m.
+
+  SMT-Lib name: `bvuaddo`.
+-/
 
 def uadd_overflow {w : Nat} (x y : BitVec w) : Bool := x.toNat + y.toNat ≥ 2 ^ w
 
-/-- Overflow predicate for signed addition on m-bit 2's complement -/
+/-- Overflow predicate for signed addition on m-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))
 
-/-- Overflow predicate for unsigned multiplication modulo 2^m -/
+/-- Overflow predicate for unsigned multiplication modulo 2^m.
+
+  SMT-Lib name: `bvumulo`.
+-/
 
 def umul_overflow {w : Nat} (x y : BitVec w) : Bool := x.toNat * y.toNat ≥ 2 ^ w
 
-/-- Overflow predicate for signed multiplication on m-bit 2's complement -/
+/-- Overflow predicate for signed multiplication on m-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))