Documentation

Lean.Meta.Tactic.Grind.Parser

Builtin parsers for grind related commands

source
def Lean.Parser.Command.grindPattern :
Parser
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Parser.Command.initGrindNorm :
    Parser
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For