Documentation

Lean.Elab.Tactic.Grind.SimprocDSL

@[reducible, inline]

Elaboration function for sym_simproc syntax.

Equations
Instances For

    Elaborate a sym_simproc syntax node into a Simproc.

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

      Elaborate a sym_discharger syntax node into a Discharger.

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