Method parse_inductive

leanr-syntax/src/parser.rs:150–186

Parse inductive declaration

(&mut self)

    /// Parse inductive declaration
    fn parse_inductive(&mut self) -> crate::Result<InductiveDecl> {
        let start = self.expect(TokenKind::Inductive)?.span;

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

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

        self.expect(TokenKind::Where)?;

        let mut constructors = Vec::new();
        while self.check(&TokenKind::Pipe) {
            self.advance();
            constructors.push(self.parse_constructor()?);
        }

        let end = if let Some(last) = constructors.last() {
            last.span
        } else {
            name.span
        };

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

    /// Parse a constructor
    fn parse_constructor(&mut self) -> crate::Result<Constructor> {