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

- Lean.Meta.Grind.markAsSimpMatchDiscrsOnly e = Lean.Meta.mkAppM `Lean.Grind.simpMatchDiscrsOnly #[e]

Instances For

source
def Lean.Meta.Grind.isSimpMatchDiscrsOnly (e : Expr) :
Bool
Equations

- Lean.Meta.Grind.isSimpMatchDiscrsOnly e = e.isAppOfArity `Lean.Grind.simpMatchDiscrsOnly 2

Instances For

source
def Lean.Meta.Grind.reduceSimpMatchDiscrsOnly :
Simp.Simproc
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.Grind.addSimpMatchDiscrsOnly (s : Simprocs) :
CoreM Simprocs

Adds `reduceSimpMatchDiscrsOnly` to `s`

Equations

- Lean.Meta.Grind.addSimpMatchDiscrsOnly s = s.add `Lean.Meta.Grind.reduceSimpMatchDiscrsOnly false

Instances For

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

Erases `Grind.simpMatchDiscrsOnly` annotations.

Equations

- One or more equations did not get rendered due to their size.

Instances For