Method parse_arrow_expr

leanr-syntax/src/parser.rs:322–338

Parse arrow type: A -> B

(&mut self)

    /// Parse arrow type: A -> B
    fn parse_arrow_expr(&mut self) -> crate::Result<Expr> {
        let mut expr = self.parse_forall_expr()?;

        while self.check(&TokenKind::Arrow) {
            let arrow_span = self.advance().span;
            let to = self.parse_forall_expr()?;
            let span = expr.span().to(to.span());

            expr = Expr::Arrow {
                span,
                from: Box::new(expr),
                to: Box::new(to),
            };
        }

        Ok(expr)
    }

    /// Parse forall: forall x : T, U
    fn parse_forall_expr(&mut self) -> crate::Result<Expr> {