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

Method expect

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

Expect a specific token

(&mut self, kind: TokenKind)

Source from the content-addressed store, hash-verified

673
674 /// Expect a specific token
675 fn expect(&mut self, kind: TokenKind) -> crate::Result<Token> {
676 if self.check(&kind) {
677 Ok(self.advance())
678 } else {
679 Err(ParseError::new(
680 self.current().span,
681 format!("Expected {:?}, found {:?}", kind, self.current().kind),
682 ))
683 }
684 }
685
686 /// Get current token
687 fn current(&self) -> &Token {

Callers 13

parse_defMethod · 0.80
parse_theoremMethod · 0.80
parse_axiomMethod · 0.80
parse_inductiveMethod · 0.80
parse_structureMethod · 0.80
parse_universe_paramsMethod · 0.80
parse_paramsMethod · 0.80
parse_forall_exprMethod · 0.80
parse_lambda_exprMethod · 0.80
parse_lambda_paramsMethod · 0.80
parse_let_exprMethod · 0.80
parse_match_exprMethod · 0.80

Calls 3

currentMethod · 0.80
checkMethod · 0.45
advanceMethod · 0.45

Tested by

no test coverage detected