hax icon indicating copy to clipboard operation
hax copied to clipboard

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

Open maximebuyse opened this issue 1 year ago • 3 comments

#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 avatar Dec 19 '24 12:12 maximebuyse

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

franziskuskiefer avatar Dec 23 '24 06:12 franziskuskiefer

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 avatar Dec 23 '24 08:12 maximebuyse

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

github-actions[bot] avatar Mar 20 '25 01:03 github-actions[bot]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

github-actions[bot] avatar Jul 17 '25 00:07 github-actions[bot]

@maximebuyse what is the status of this issue?

W95Psp avatar Jul 17 '25 08:07 W95Psp

@maximebuyse what is the status of this issue?

Still relevant

maximebuyse avatar Jul 17 '25 08:07 maximebuyse

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

github-actions[bot] avatar Sep 18 '25 00:09 github-actions[bot]