def Lean.Elab.elabSimprocPattern (stx : Lean.Syntax) : Lean.MetaM Lean.Expr

Equations

• Lean.Elab.elabSimprocPattern stx = (do let pattern ← Lean.Elab.Term.elabTerm stx none Lean.Elab.Term.synthesizeSyntheticMVars pure pattern).run'

def Lean.Elab.elabSimprocKeys (stx : Lean.Syntax) : Lean.MetaM (Array Lean.Meta.SimpTheoremKey)

Equations

• Lean.Elab.elabSimprocKeys stx = do let pattern ← Lean.Elab.elabSimprocPattern stx Lean.Meta.withSimpGlobalConfig (Lean.Meta.DiscrTree.mkPath pattern)

def Lean.Elab.checkSimprocType (declName : Lean.Name) : Lean.CoreM Bool

Equations

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

def Lean.Elab.Command.elabSimprocPattern : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabSimprocPatternBuiltin : Lean.Elab.Command.CommandElab

Equations

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