Implement return / break / continue loop fold operators for f*
#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).
How is this related to #1171? The description here sounds like this should be working for while loops.
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.
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.
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.
@maximebuyse what is the status of this issue?
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.