Method parse_theorem

leanr-syntax/src/parser.rs:102–125

Parse theorem declaration

(&mut self)

    /// Parse theorem declaration
    fn parse_theorem(&mut self) -> crate::Result<TheoremDecl> {
        let start = self.expect(TokenKind::Theorem)?.span;

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

        self.expect(TokenKind::Colon)?;
        let type_ = Box::new(self.parse_expr()?);

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

        let end = proof.span();

        Ok(TheoremDecl {
            span: start.to(end),
            name,
            universe_params,
            params,
            type_,
            proof,
        })
    }

    /// Parse axiom declaration
    fn parse_axiom(&mut self) -> crate::Result<AxiomDecl> {