forked from rust-lang/rust-analyzer
-
Notifications
You must be signed in to change notification settings - Fork 11
Open
Description
Currently verus-analyzer expects at least one Expr in each clause:
verus-analyzer/crates/syntax/rust.ungram
Lines 760 to 767 in 9f98767
| RequiresClause = | |
| 'requires' (Expr (',' Expr)* ','?) | |
| EnsuresClause = | |
| 'ensures' (Expr (',' Expr)* ','?) | |
| DefaultEnsuresClause = | |
| 'default_ensures' (Expr (',' Expr)* ','?) |
However, verus_syn accepts empty clauses, and that's confirmed to be intentional.
The goal here is to bring verus-analyzer's grammar in sync with verus_syn's.
See discussion here:
verus-lang/verus#2098 (comment)
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels