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

Implement return / break / continue loop fold operators for f* #1204

Open
maximebuyse opened this issue Dec 19, 2024 · 2 comments
Open

Implement return / break / continue loop fold operators for f* #1204

maximebuyse opened this issue Dec 19, 2024 · 2 comments
Assignees
@maximebuyse
Labels
f* F* backend libcore

Comments

@maximebuyse
Copy link
Contributor

maximebuyse commented Dec 19, 2024 •
edited by W95Psp
Loading

#988 introduced new fold operators (a _cf and _return version for fold_enumerated_chunked_slice, fold_enumerated_slice, fold_range_step_by, fold_range, Core__iter__traits__iterator__Iterator__fold, while_loop) but they are not provided by the fstar core lib. We should provide a definition for each of them (it can even be an assume val for the beginning).
@maximebuyse maximebuyse added f* F* backend libcore labels Dec 19, 2024
@franziskuskiefer
Copy link
Member

How is this related to #1171? The description here sounds like this should be working for while loops.

@maximebuyse
Copy link
Contributor Author

How is this related to #1171? The description here sounds like this should be working for while loops.

I don't think they are related.

@maximebuyse maximebuyse mentioned this issue Dec 23, 2024
Open
@maximebuyse maximebuyse self-assigned this Dec 23, 2024
@franziskuskiefer franziskuskiefer mentioned this issue Jan 14, 2025
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@maximebuyse maximebuyse

Labels
f* F* backend libcore
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@franziskuskiefer @maximebuyse