Apply suggestions from code review

Co-authored-by: Tobias Grosser <[email protected]>
opencompl · Sep 4, 2024 · d3ad6b5 · d3ad6b5
1 parent f9efb1d
commit d3ad6b5
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
@@ -612,7 +612,7 @@ def concat {n} (msbs : BitVec n) (lsb : Bool) : BitVec (n+1) := msbs ++ (ofBool
 
 /--
 `x.shiftConcat b` shifts all bits of `x` to the left by `1` and sets the least significant bit to `b`.
-It is a non dependent version of `concat` that does not change the total bitwidth.
+It is a non-dependent version of `concat` that does not change the total bitwidth.
 -/
 def shiftConcat (x : BitVec n) (b : Bool) : BitVec n :=
   x <<< 1 ||| (ofBool b).zeroExtend n

diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
@@ -513,7 +513,7 @@ structure DivModState (w : Nat) : Type where
   /-- The current remainder. -/
   r : BitVec w
 
-/-- A `DivModState` is lawful if the remainder width `wr` plus the dividiend width `wn` equals `w`,
+/-- A `DivModState` is lawful if the remainder width `wr` plus the dividend width `wn` equals `w`,
 and that the bitvectors `r` and `n` have values in these bounds given these bitwidths.
 
 This is a proof engineering choice: An alternative world could have