From 8c3448f146137e074ea771b83a0a5f777db1a102 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Tue, 14 Jan 2025 10:21:22 +0000 Subject: [PATCH] chore: fix docstrings --- src/Init/Data/BitVec/Basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index e652f148081..0e16c7bc1bf 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -676,28 +676,28 @@ def ofBoolListLE : (bs : List Bool) → BitVec bs.length 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^w. 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 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)) -/-- Overflow predicate for unsigned multiplication modulo 2^m. +/-- 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 -/-- Overflow predicate for signed multiplication on m-bit 2's complement. +/-- Overflow predicate for signed multiplication on w-bit 2's complement. SMT-Lib name: `bvsmulo`. -/