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.

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

              Adds reduceSimpMatchDiscrsOnly to s

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

                  Erases Grind.simpMatchDiscrsOnly annotations.

                  Equations
                    Instances For