From 8dba084ce8d9053351a295857579ecdacb3ae2a3 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Thu, 26 Sep 2024 04:09:59 +0100 Subject: [PATCH] chore: improve wording in comment --- src/Init/Data/BitVec/Bitblast.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 033239f1a03e..e03f009337a8 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -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`.