Documentation

Lean.Parser.StrInterpolation

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

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 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)