def Lean.Parser.isQuotableCharForStrInterpolant (c : Char) : Bool

Equations

• Lean.Parser.isQuotableCharForStrInterpolant c = (c == Char.ofNat 123 || Lean.Parser.isQuotableCharDefault c)

def Lean.Parser.interpolatedStrFn (p : Lean.Parser.ParserFn) : Lean.Parser.ParserFn

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Parser.interpolatedStrFn.parse (p : Lean.Parser.ParserFn) (input : String) (stackSize : Nat) (startPos : String.Pos) (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

@[inline]

def Lean.Parser.interpolatedStrNoAntiquot (p : Lean.Parser.Parser) : Lean.Parser.Parser

Equations

• Lean.Parser.interpolatedStrNoAntiquot p = { info := Lean.Parser.mkAtomicInfo "interpolatedStr", fn := Lean.Parser.interpolatedStrFn (Lean.Parser.withoutPosition p).fn }

def Lean.Parser.interpolatedStr (p : Lean.Parser.Parser) : Lean.Parser.Parser

Equations

• Lean.Parser.interpolatedStr p = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "interpolatedStr" Lean.interpolatedStrKind true) (Lean.Parser.interpolatedStrNoAntiquot p)