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
[Merged by Bors] - chore(data/seq/seq): use terminates
predicate in to_list_or_stream
#15826
Conversation
this is not constructively possible.) -/ | ||
def to_list_or_stream (s : seq α) [decidable (∃ n, ¬ (nth s n).is_some)] : | ||
list α ⊕ stream α := | ||
if h : ∃ n, ¬ (nth s n).is_some | ||
def to_list_or_stream (s : seq α) [decidable s.terminates] : list α ⊕ stream α := |
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.
It might be worth providing an instance along the lines of
instance [decidable (∃ n, ¬ (nth s n).is_some)] : decidable s.terminates :=
but I guess if nothing uses this function anyway it's may best to leave it until an actual example appears.
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.
Yes, this is currently unused.
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.
bors d+
✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
bors r+ |
#15826) We already have a canonical way to spell out that a sequence terminates, so we don't need to spell it in full.
Pull request successfully merged into master. Build succeeded: |
terminates
predicate in to_list_or_stream
terminates
predicate in to_list_or_stream
We already have a canonical way to spell out that a sequence terminates, so we don't need to spell it in full.