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.isSimpMatchDiscrsOnly (e : Expr) : Bool

Equations

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

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) : MetaM Simp.Result

Erases Grind.simpMatchDiscrsOnly annotations.

Equations

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