Parse a single declaration
(&mut self)
| 53 | |
| 54 | /// Parse a single declaration |
| 55 | pub fn parse_decl(&mut self) -> crate::Result<Decl> { |
| 56 | let token = self.current(); |
| 57 | |
| 58 | match &token.kind { |
| 59 | TokenKind::Def => Ok(Decl::Def(self.parse_def()?)), |
| 60 | TokenKind::Theorem => Ok(Decl::Theorem(self.parse_theorem()?)), |
| 61 | TokenKind::Axiom => Ok(Decl::Axiom(self.parse_axiom()?)), |
| 62 | TokenKind::Inductive => Ok(Decl::Inductive(self.parse_inductive()?)), |
| 63 | TokenKind::Structure => Ok(Decl::Structure(self.parse_structure()?)), |
| 64 | _ => Err(ParseError::new( |
| 65 | token.span, |
| 66 | format!("Expected declaration, found {:?}", token.kind), |
| 67 | )), |
| 68 | } |
| 69 | } |
| 70 | |
| 71 | /// Parse def declaration: def name params : type := body |
| 72 | fn parse_def(&mut self) -> crate::Result<DefDecl> { |
no test coverage detected