Skip to content

Commit

Permalink
chore: improve wording in comment
Browse files Browse the repository at this point in the history
  • Loading branch information
tobiasgrosser committed Sep 26, 2024
1 parent 0634588 commit 8dba084
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Init/Data/BitVec/Bitblast.lean
Original file line number Diff line number Diff line change
Expand Up @@ -454,7 +454,7 @@ such that `(d * q + r)` overflows and wraps around to equal `n`.
This tells us that the division algorithm must have more restrictions than just the ones
we have for integers. These restrictions are captured in `DivModState.Lawful`.
The key idea is to state the relationship in terms of the `{n, d, q, r}.toNat` values.
The key idea is to state the relationship in terms of the toNat values of {n, d, q, r}.
If the division equation `d.toNat * q.toNat + r.toNat = n.toNat` holds,
then `n.udiv d = q` and `n.umod d = r`.
Expand Down

0 comments on commit 8dba084

Please sign in to comment.