Defines the include_str macro.

ink

def Mathlib.Util.includeStr : Lean.ParserDescr

A term macro that includes the content of a file, as a string.

Equations

• Mathlib.Util.includeStr = Lean.ParserDescr.node `Mathlib.Util.includeStr 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "include_str ") (Lean.ParserDescr.const `str))