Deprecating :heapQuantifier; small documentation tasks #3456
Conversation
There was a problem hiding this comment.
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.
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.
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.
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.
Co-authored-by: Rustan Leino <leino@amazon.com>
Co-authored-by: Rustan Leino <leino@amazon.com>
Co-authored-by: Rustan Leino <leino@amazon.com>
Co-authored-by: Rustan Leino <leino@amazon.com>
Co-authored-by: Rustan Leino <leino@amazon.com>
Co-authored-by: Rustan Leino <leino@amazon.com>
Co-authored-by: Rustan Leino <leino@amazon.com>
Co-authored-by: Rustan Leino <leino@amazon.com>
Co-authored-by: Rustan Leino <leino@amazon.com>
Co-authored-by: Rustan Leino <leino@amazon.com>
Co-authored-by: Rustan Leino <leino@amazon.com>
Co-authored-by: Rustan Leino <leino@amazon.com>
Co-authored-by: Rustan Leino <leino@amazon.com>
Co-authored-by: Rustan Leino <leino@amazon.com>
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 <davidcok@github.com>
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.