Documentation

Lean.Meta.Tactic.Grind.MatchDiscrOnly

Returns Grind.simpMatchDiscrsOnly e. Recall that Grind.simpMatchDiscrsOnly is a gadget for instructing the grind simplifier to only normalize/simplify the discriminants of a match-expression. See reduceSimpMatchDiscrsOnly.

Equations
    Instances For
      Equations
        Instances For

          Erases Grind.simpMatchDiscrsOnly annotations.

          Equations
            Instances For