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]

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

Equations

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

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

def Lean.Meta.Grind.eraseSimpMatchDiscrsOnly (e : Expr) : CoreM Expr

Erases Grind.simpMatchDiscrsOnly annotations.

Equations

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