search

verus-lang / verus

Verified Rust for low-level systems code
MIT License
1.06k stars 58 forks source link

Implement repeat for the seq macro #1178

Closed jaybosamiya-ms closed 1 week ago

jaybosamiya-ms commented 1 week ago

Finishes off one of the tasks on https://github.com/verus-lang/verus/discussions/1176?sort=top#discussioncomment-9875969

utaal commented 6 days ago

Can you briefly summarize what was the test failure we were seeing and how it was fixed? Thanks!

jaybosamiya-ms commented 5 days ago

It was an issue of functions/closures/funspec. In particular, throwing away the passed-in-argument via _ is considered an advanced pattern by Verus (in the style of general parameter pattern binds, such as (a, b) or such), and thus not available in spec land, but we can just bind it to an unused variable (_x), which lets it go through.

Essentially, the code change:

- $crate::vstd::seq::Seq::new($n, |_| $elem)
+ $crate::vstd::prelude::closure_to_fn_spec(|_x: _| $elem),

The error message was confusing for a while, but once I realized that the issue was the _, and switched it to _x, it was much more straightforward to realize that I also needed to wrap it with the closure_to_fn_spec

utaal commented 5 days ago

Aha! Thanks for the explanation.