-
Notifications
You must be signed in to change notification settings - Fork 257
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Deprecating :heapQuantifier; small documentation tasks #3456
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I commented on many coding style and code font issues, but I may have missed some. Also, I'm suggest renaming some of the identifiers--it's nice if the actuals have different names from the formals, but since the current names of the actuals would be hard to understand without more context, I suggest simplifying them to other, plausible names.
@@ -61,7 +62,7 @@ There are also publications and lecture notes: | |||
* Videos at [Verification Corner](https://www.youtube.com/channel/UCP2eLEql4tROYmIYm5mA27A) | |||
|
|||
And some books: | |||
* K. Rustan M. Leino, 2023, [_Program Proofs_](https://mitpress.mit.edu/9780262546232/program-proofs/), to be available in 2023. | |||
* K. Rustan M. Leino, 2023, [_Program Proofs_](https://mitpress.mit.edu/9780262546232/program-proofs/), available March, 2023. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
On the subsequent line, I suggest either removing the bullet about the draft version from Lulu or stating that it is available only until the MIT Press version comes out.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Modified but left in, just until the book is for sure available.
Being “injective” is the mathematical description of any function f that satisfies the property you’re giving in the precondition. | ||
Another name for “injective” is “one-to-one” (which sounds more symmetric than it is--hence, the name “injective” is probably better). |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think there's any reason to mention "injectivity" and "one-to-one" in this answer, since the question and the rest of the answer don't make use of these definitions.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Removed
Co-authored-by: Rustan Leino <[email protected]>
Co-authored-by: Rustan Leino <[email protected]>
Co-authored-by: Rustan Leino <[email protected]>
Co-authored-by: Rustan Leino <[email protected]>
Co-authored-by: Rustan Leino <[email protected]>
Co-authored-by: Rustan Leino <[email protected]>
Co-authored-by: Rustan Leino <[email protected]>
Co-authored-by: Rustan Leino <[email protected]>
Co-authored-by: Rustan Leino <[email protected]>
Co-authored-by: Rustan Leino <[email protected]>
Co-authored-by: Rustan Leino <[email protected]>
Co-authored-by: Rustan Leino <[email protected]>
Co-authored-by: Rustan Leino <[email protected]>
Co-authored-by: Rustan Leino <[email protected]>
Fixes #3398 Follows on #3456 <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: davidcok <[email protected]>
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.