Skip to content

Commit cadde2f

Browse files
committed
Fix a stale link for the math.integer.isqrt correctness proof
1 parent bff0051 commit cadde2f

1 file changed

Lines changed: 2 additions & 3 deletions

File tree

Modules/mathintegermodule.c

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -180,10 +180,9 @@ that the bound `(a - 1)**2 < (n >> s) < (a + 1)**2` is maintained from one
180180
iteration to the next. A sketch of the proof of this is given below.
181181
182182
In addition to the proof sketch, a formal, computer-verified proof
183-
of correctness (using Lean) of an equivalent recursive algorithm can be found
184-
here:
183+
of correctness (using Lean) of the algorithm can be found here:
185184
186-
https://github.com/mdickinson/snippets/blob/master/proofs/isqrt/src/isqrt.lean
185+
https://github.com/mdickinson/snippets/tree/main/proofs/isqrt
187186
188187
189188
Here's Python code equivalent to the C implementation below:

0 commit comments

Comments
 (0)