Method parse_forall_expr

leanr-syntax/src/parser.rs:341–353

Parse forall: forall x : T, U

(&mut self)

    /// Parse forall: forall x : T, U
    fn parse_forall_expr(&mut self) -> crate::Result<Expr> {
        if self.check(&TokenKind::Forall) {
            let start = self.advance().span;
            let params = self.parse_params()?;
            self.expect(TokenKind::Comma)?;
            let body = Box::new(self.parse_expr()?);
            let span = start.to(body.span());

            Ok(Expr::Forall { span, params, body })
        } else {
            self.parse_lambda_expr()
        }
    }

    /// Parse lambda: fun x => body
    fn parse_lambda_expr(&mut self) -> crate::Result<Expr> {