MCPcopy Create free account
hub / github.com/agenticsorg/lean-agentic / parse_ident

Method parse_ident

leanr-syntax/src/parser.rs:651–664  ·  view source on GitHub ↗

Parse an identifier

(&mut self)

Source from the content-addressed store, hash-verified

649
650 /// Parse an identifier
651 fn parse_ident(&mut self) -> crate::Result<Ident> {
652 match &self.current().kind {
653 TokenKind::Ident(name) => {
654 let span = self.current().span;
655 let name = name.clone();
656 self.advance();
657 Ok(Ident::new(name, span))
658 }
659 _ => Err(ParseError::new(
660 self.current().span,
661 format!("Expected identifier, found {:?}", self.current().kind),
662 )),
663 }
664 }
665
666 /// Check if current token matches
667 fn check(&self, kind: &TokenKind) -> bool {

Callers 10

parse_defMethod · 0.80
parse_theoremMethod · 0.80
parse_axiomMethod · 0.80
parse_inductiveMethod · 0.80
parse_constructorMethod · 0.80
parse_structureMethod · 0.80
parse_universe_paramsMethod · 0.80
parse_paramsMethod · 0.80
parse_lambda_paramsMethod · 0.80
parse_let_exprMethod · 0.80

Calls 3

currentMethod · 0.80
cloneMethod · 0.45
advanceMethod · 0.45

Tested by

no test coverage detected