Method parse_def

leanr-syntax/src/parser.rs:72–99

Parse def declaration: def name params : type := body

(&mut self)

    /// Parse def declaration: def name params : type := body
    fn parse_def(&mut self) -> crate::Result<DefDecl> {
        let start = self.expect(TokenKind::Def)?.span;

        let name = self.parse_ident()?;
        let universe_params = self.parse_universe_params()?;
        let params = self.parse_params()?;

        let return_type = if self.check(&TokenKind::Colon) {
            self.advance();
            Some(Box::new(self.parse_expr()?))
        } else {
            None
        };

        self.expect(TokenKind::ColonEq)?;
        let body = Box::new(self.parse_expr()?);

        let end = body.span();

        Ok(DefDecl {
            span: start.to(end),
            name,
            universe_params,
            params,
            return_type,
            body,
        })
    }

    /// Parse theorem declaration
    fn parse_theorem(&mut self) -> crate::Result<TheoremDecl> {