Documentation

Lean.Meta.Tactic.Grind.MatchDiscrOnly

source
def Lean.Meta.Grind.markAsSimpMatchDiscrsOnly (e : Expr) :
MetaM Expr

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.

Instances For
    source
    def Lean.Meta.Grind.isSimpMatchDiscrsOnly (e : Expr) :
    Bool
    Instances For
      source
      def Lean.Meta.Grind.reduceSimpMatchDiscrsOnly :
      Simp.Simproc
      Instances For
        source
        def Lean.Meta.Grind.addSimpMatchDiscrsOnly (s : Simprocs) :
        CoreM Simprocs

        Adds reduceSimpMatchDiscrsOnly to s

        Instances For
          source
          def Lean.Meta.Grind.eraseSimpMatchDiscrsOnly (e : Expr) :
          MetaM Simp.Result

          Erases Grind.simpMatchDiscrsOnly annotations.

          Instances For