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.

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

feat(lib) New sandwich core changes #1192

Open
wants to merge 9 commits into
base: main
Choose a base branch
from
Prev Previous commit
Next Next commit
Rename into_iterator to t_IntoIterator to help type class inference.
maximebuyse committed Jan 8, 2025
commit 86e9b680fdd51f5de5db40d51d0361785940e025
6 changes: 2 additions & 4 deletions proof-libs/fstar/core/Core.Iter.Traits.Collect.fst
Original file line number Diff line number Diff line change
@@ -1,14 +1,12 @@
module Core.Iter.Traits.Collect

class into_iterator self = {
class t_IntoIterator self = {
f_IntoIter: Type0;
// f_Item: Type0;
f_into_iter: self -> f_IntoIter;
}

let t_IntoIterator = into_iterator

unfold instance impl t {| Core.Iter.Traits.Iterator.iterator t |}: into_iterator t = {
unfold instance impl t {| Core.Iter.Traits.Iterator.iterator t |}: t_IntoIterator t = {
f_IntoIter = t;
f_into_iter = id;
}