Equations
Equations
- Lean.Parser.interpolatedStrFn p c s = let input := c.toInputContext.input; let stackSize := Lean.Parser.ParserState.stackSize s; (fun parse => let startPos := s.pos; if String.atEnd input startPos = true then Lean.Parser.ParserState.mkEOIError s else let curr := String.get input s.pos; if (curr != Char.ofNat 34) = true then Lean.Parser.ParserState.mkError s "interpolated string" else let s := Lean.Parser.ParserState.next s input startPos; parse startPos c s) (Lean.Parser.interpolatedStrFn.parse p input stackSize)
partial def
Lean.Parser.interpolatedStrFn.parse
(p : Lean.Parser.ParserFn)
(input : String)
(stackSize : Nat)
(startPos : Nat)
(c : Lean.Parser.ParserContext)
(s : Lean.Parser.ParserState)
:
@[inline]
Equations
- Lean.Parser.interpolatedStrNoAntiquot p = { info := Lean.Parser.mkAtomicInfo "interpolatedStr", fn := Lean.Parser.interpolatedStrFn p.fn }