hacspec
F*: interface mode: missed binders
In F*, binders val declarations cannot be patterns.
In the interface mode, we generate val declarations out of Rust functions possibly annotated with pre- or post-conditions.
Rust functions accept any pattern on function inputs. If a binding introduced by a pattern happens to be used in a post or a pre, currently, this produces bad F* code.
We should give non-trivial patterns (e.g. not variable patterns) names and rewrite pre and post-condition.
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](https://avatars.githubusercontent.com/in/15368?v=4 "Published by a pub.dev verified publisher"){kind=small}
This is still relevant. This transformation should be done outside of the backend, as a phase.
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 closed due to a lack of activity since being marked as stale. If you believe this issue is still relevant, please reopen it with an update or comment.
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.
