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

Equations

• Lean.Parser.isQuotableCharForStrInterpolant c = (c == '{' || Lean.Parser.isQuotableCharDefault c)

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

Equations

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

@[inline]

def Lean.Parser.interpolatedStrNoAntiquot (p : 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 : Parser) : Parser

The parser interpolatedStr(p) parses a string literal like "foo" (see str), but the string may also contain {} escapes, and within the escapes the parser p is used. For example, interpolatedStr(term) will parse "foo {2 + 2}", where 2 + 2 is parsed as a term rather than as a string. Note that the full Lean term grammar is available here, including string literals, so for example "foo {"bar" ++ "baz"}" is a legal interpolated string (which evaluates to foo barbaz).

This parser has arity 1, and returns a interpolatedStrKind with an odd number of arguments, alternating between chunks of literal text and results from p. The literal chunks contain uninterpreted substrings of the input. For example, "foo\n{2 + 2}" would have three arguments: an atom "foo\n{, the parsed 2 + 2 term, and then the atom }".

Equations

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