hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
200 stars 21 forks source link

Phase to desugar as patterns (`x @ subpattern`) #833

Open W95Psp opened 3 months ago

W95Psp commented 3 months ago

Some backends (e.g. F*) don't support as patterns, and reject them. For instance:

fn f(x: Option<u8>) -> u8 {
    match x {
        _binder @ Some(x) => x,
        _ => 0,
    }
}

We should have a phase that rewrites such matches. With the new phase @maximebuyse added that rewrites if let-guards, this comes for almost free: we could for instance rewrite binder @ Some(x) as binder if let Some(x) = binder.

github-actions[bot] commented 1 month ago

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.

W95Psp commented 1 month ago

Still relevant