Add documentation on type sizes #1188
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
hayley-leblanc
force-pushed
the
type_size_docs
branch
from
c7c8b21
to
ca0ed8f
Compare
|
This is a bit redundant with existing layout documentation (https://verus-lang.github.io/verus/guide/reference-global.html) However, the existing page lacks examples, which this PR provides. I realized it's been a few months, but if you're still interested in merging this, I think the best course is to rebase and consolidate the new examples into the existing |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds a new page to the docs with info on setting the size of
Sizedtypes for use in ghost code, including how to set the size ofusize/isize. There was a small amount of documentation onusize/isizein the the Integers part of the tutorial, so to make it easier to keep the documentation in sync I moved this to the new file. I'm not sure whether it would be better to have this information in the tutorial or the reference, though, so I'm happy to move some/all of the documentation back to the tutorial if folks think that would be a better location for it.