From e43dc4f0ae0a8fe84eecb5925785d090a5f89a67 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 3 Apr 2024 11:34:59 -0400
Subject: [PATCH] Address review comments

---
 .hlint.yaml                  |  6 ------
 what4/src/What4/Interface.hs | 11 ++++++-----
 2 files changed, 6 insertions(+), 11 deletions(-)

diff --git a/.hlint.yaml b/.hlint.yaml
index 3060dc3f..db24bf8b 100644
--- a/.hlint.yaml
+++ b/.hlint.yaml
@@ -12,9 +12,3 @@
     name: Use bvOne
     lhs: "What4.Interface.bvLit sym w (Data.BitVector.Sized.one w)"
     rhs: 'What4.Interface.bvOne sym w'
-
-# TODO:
-# - error:
-#     name: Use PP.viaShow
-#     lhs: "Prettyprinter.pretty (show x)"
-#     rhs: 'Prettyprinter.viaShow x'
diff --git a/what4/src/What4/Interface.hs b/what4/src/What4/Interface.hs
index 1cffa8bf..9b3a5299 100644
--- a/what4/src/What4/Interface.hs
+++ b/what4/src/What4/Interface.hs
@@ -156,6 +156,10 @@ module What4.Interface
   , SymEncoder(..)
 
     -- * Utility combinators
+    -- ** Bitvector operations
+  , bvZero
+  , bvOne
+
     -- ** Boolean operations
   , backendPred
   , andAllOf
@@ -180,10 +184,6 @@ module What4.Interface
     -- * Exceptions
   , InvalidRange(..)
 
-    -- * Bitvector utilities
-  , bvZero
-  , bvOne
-
     -- * Reexports
   , module Data.Parameterized.NatRepr
   , module What4.BaseTypes
@@ -1121,7 +1121,7 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym), HashableF (BoundVar sym)
   -- | Return the bitvector of the desired width with all 0 bits;
   --   this is the minimum unsigned integer.
   minUnsignedBV :: (1 <= w) => sym -> NatRepr w -> IO (SymBV sym w)
-  minUnsignedBV sym w = bvZero sym w
+  minUnsignedBV sym w = bvLit sym w (BV.zero w)
 
   -- | Return the bitvector of the desired width with all bits set;
   --   this is the maximum unsigned integer.
@@ -3309,5 +3309,6 @@ zeroStatistics = Statistics { statAllocs = 0
 bvZero :: (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> IO (SymBV sym w)
 bvZero = minUnsignedBV
 
+-- | A bitvector that is all zeroes except the LSB, which is one.
 bvOne :: (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> IO (SymBV sym w)
 bvOne sym w = bvLit sym w (BV.one w)