Apply suggestions from code review

Co-authored-by: Siddharth <[email protected]>
leanprover · Oct 7, 2024 · 77bd117 · 77bd117
1 parent 64fdac3
commit 77bd117
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
@@ -78,7 +78,7 @@ def toString : BVBinOp → String
   | xor => "^"
   | add => "+"
   | mul => "*"
-  | udiv => "u/"
+  | udiv => "/ᵤ"
 
 instance : ToString BVBinOp := ⟨toString⟩
 

diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean
@@ -13,7 +13,7 @@ import Std.Sat.AIG.If
 
 /-!
 This module contains the implementation of a bitblaster for `BitVec.udiv`. The implemented
-circuit is a ripple carry adder.
+circuit is a shift subtractor.
 -/
 
 namespace Std.Tactic.BVDecide