Documentation

Lean.ParserCompiler

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

Instances For
    Equations
    • ctx.tyName = ctx.categoryAttr.defn.valueTypeName
    Instances For

      Replace all references of Parser with tyName

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

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

        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.

        Precondition: α must match ctx.tyName.

        Instances For