stacksTagFn — Mathlib

Lean4
/-- The main parser for Stacks Project Tags: it accepts any sequence of 4 digits or
uppercase letters. -/
def stacksTagFn : ParserFn := fun c s =>
  let i := s.pos
  let s := takeWhileFn (fun c => c.isAlphanum) c s
  if s.hasError then s
  else
    if s.pos == i then ParserState.mkError s "stacks tag"
    else
      let tag := c.extract i s.pos
      if !tag.all fun c => c.isDigit || c.isUpper then
        ParserState.mkUnexpectedError s "Stacks tags must consist only of digits and uppercase letters."
      else
        if tag.length != 4 then ParserState.mkUnexpectedError s "Stacks tags must be exactly 4 characters"
        else mkNodeToken stacksTagKind i true c s
Похожие утверждения