Task 87 #28
Task 87 #28
Conversation
There was a problem hiding this comment.
Very nice! This is quite complex to specify. One thing that the prompt doesn't specify at all, but that a user of this code might expect, would be that the entries in coords are distinct. This is already implied by the combination of row_sorted_asc and row_col_sorted_desc (and the fact that the later uses strict inequality), so you could leave that implicit or you could write a (hopefully short) lemma showing that's the case.
tasks/human_eval_087.rs
Outdated
| } | ||
|
|
||
| /// Returns lst as a Seq. | ||
| pub open spec fn lst_seq_refl(lst: Vec<Vec<i32>>) -> Seq<Seq<i32>> { |
There was a problem hiding this comment.
This isn't very discoverable at the moment, unfortunately, but I think this function is equivalent to doing lst.deep_view(). Looking at the source for the DeepView trait shows more details.
There was a problem hiding this comment.
If changing to deep_view breaks a bunch of proofs, it's probably not worth changing at this point. Just a note for the future.
|
Very nice! Sorry, I didn't realize you had pushed changes since I reviewed the initial PR. I'll merge this in. |
No description provided.