Documentation

Lean.ParserCompiler

Gadgets for compiling parser declarations into other programs, such as pretty printers.

Instances For
    Equations
      Instances For

        Replace all references of Parser with tyName

        Equations
          Instances For

            Takes an expression of type Parser, and determines the syntax kind of the root node it produces.

            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.

            Equations
              Instances For

                Precondition: α must match ctx.tyName.

                Equations
                  Instances For