parse a paren-delimited expression
(&mut self)
| 260 | } |
| 261 | /// parse a paren-delimited expression |
| 262 | fn parse_primary(&mut self) -> syn::Result<AssertionWithoutId> { |
| 263 | if let Some(stream) = self.consume_group(Delimiter::Parenthesis) { |
| 264 | self.from_token_stream_last_span(stream).extract_assertion() |
| 265 | } else if self.consume_keyword("forall") { |
| 266 | if let Some(stream) = self.consume_group(Delimiter::Parenthesis) { |
| 267 | self.from_token_stream_last_span(stream).extract_quantifier_rhs(false) |
| 268 | } else { |
| 269 | Err(self.error_expected("`(`")) |
| 270 | } |
| 271 | } else if self.consume_keyword("exists") { |
| 272 | if let Some(stream) = self.consume_group(Delimiter::Parenthesis) { |
| 273 | self.from_token_stream_last_span(stream).extract_quantifier_rhs(true) |
| 274 | } else { |
| 275 | Err(self.error_expected("`(`")) |
| 276 | } |
| 277 | } else { |
| 278 | Err(self.error_expected("`(`, `forall` or `exists`")) |
| 279 | } |
| 280 | } |
| 281 | fn extract_quantifier_rhs(&mut self, exists: bool) -> syn::Result<AssertionWithoutId> { |
| 282 | if !self.consume_operator("|") { |
| 283 | return Err(self.error_expected("`|`")); |
no test coverage detected