hacspec
Empty clauses in match generate syntactically ill-formed code in F*
As shown in this playground, the following (valid) rust code :
fn main () -> i32 {
match (1,2) {
| (x, y) => y , /* note the | before the clause */
}
}
generates the ill-formed fstar code:
let main (_: Prims.unit) : i32 =
match
mk_i32 1, mk_i32 2 <: (i32 & i32)
with
| | x, y -> y (* double | | , ill formed *)
The empty clause is translated as an empty clause.
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 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.
In the THIR importer, Or clauses with a single clause should be normalized.