Skip to content
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.

Sign up for GitHub

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

Jump to bottom

docs: Completed (and corrected) IteratorSpec section #1842

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

docs: Completed (and corrected) IteratorSpec section #1842

Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7fc7646
Completed (and corrected) IteratorSpec section
robin-aws Feb 19, 2022
6527461
Missing saved changes
robin-aws Feb 19, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Missing saved changes
  • Loading branch information
@robin-aws
robin-aws committed Feb 19, 2022
commit 652746130743ea1731b206cc602fbf7417a23297
5 changes: 4 additions & 1 deletion docs/DafnyRef/Specifications.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -531,7 +531,10 @@ in an iterator's body, while `ensures` clauses must hold when the
body completes.

Note also that all iterators define an implicit `Valid()` predicate
that is
that is used as a pre-condition for `MoveNext`. An iterator is only
guaranteed to be `Valid()` after invoking `MoveNext` if that method
Comment on lines +534 to +535
Copy link
Collaborator

Choose a reason for hiding this comment

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

I suggest moving the "only" to just before the "if"

returns `true`, which prevents you from attempting to move to any
additional elements once the iterator has terminated.

The following table summarized how these clauses are translated into
the iterator type:
Expand Down