Skip to content

Fixed mistake in "Putting it all together" page in docs#2247

Merged
parno merged 2 commits intoverus-lang:mainfrom
jsenn:user/jsenn/doc-fix
Mar 19, 2026
Merged

Fixed mistake in "Putting it all together" page in docs#2247
parno merged 2 commits intoverus-lang:mainfrom
jsenn:user/jsenn/doc-fix

Conversation

@jsenn
Copy link
Contributor

@jsenn jsenn commented Mar 14, 2026

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

Copy link
Collaborator

@parno parno left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for catching this! What if we used text like this?

To keep the overflow reasoning simple, we add a precondition to loop_triangle saying that the result needs to fit within a u32.

I think something like the initial clause is needed to imply that this is a somewhat artificial precondition (we're asking the caller to establish a bound on the final value, but presumably it's calling this function because it doesn't know the actual value!).

I'd also be inclined to simplify the code by replacing < 0x1_0000_0000 with <+ u32::MAX. I think that would make the intent of the property clearer.

What do you think?

@tjhance
Copy link
Collaborator

tjhance commented Mar 18, 2026

I agree we should use u32::MAX, it's helpful for users to know that they can use those

Also reworded doc text per suggestion from @parno.
@jsenn jsenn force-pushed the user/jsenn/doc-fix branch from bd3665d to 9d9eec5 Compare March 18, 2026 21:04
@jsenn
Copy link
Contributor Author

jsenn commented Mar 18, 2026

Updated the text per @parno's suggestion and changed the recursion example to use u32::MAX throughout instead of the magic number.

This probably should've been an issue not a PR so you could word things how you want, sorry about that.

@parno
Copy link
Collaborator

parno commented Mar 19, 2026

Thanks for making the updates! I think it looks good now.

This probably should've been an issue not a PR so you could word things how you want, sorry about that.

No worries -- we appreciate contributions in all forms :)

@parno parno merged commit 329f8b5 into verus-lang:main Mar 19, 2026
13 checks passed
@tjhance
Copy link
Collaborator

tjhance commented Mar 19, 2026

yes, PRs are a perfectly fine way to iterate on minor changes

@jsenn jsenn deleted the user/jsenn/doc-fix branch March 19, 2026 12:46
@jaylorch
Copy link
Collaborator

Should this use <= u32::MAX instead of < u32::MAX?

@jsenn
Copy link
Contributor Author

jsenn commented Mar 20, 2026

Should this use <= u32::MAX instead of < u32::MAX?

yes it should, good catch: #2256

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants