Gadgets for compiling parser declarations into other programs, such as pretty printers.
- varName : Name
- categoryAttr : KeyedDeclsAttribute α
- combinatorAttr : CombinatorAttribute
Instances For
Equations
Instances For
partial def
Lean.ParserCompiler.compileParserExpr
{α : Type}
(ctx : Context α)
(builtin force : Bool)
(e : Expr)
:
Translate an expression of type Parser
into one of type tyName
, tagging intermediary constants with
ctx.combinatorAttr
. If force
is false
, refuse to do so for imported constants.