def Lean.Elab.elabSimprocPattern (stx : Syntax) : MetaM 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 : Syntax) : MetaM (Array 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 : Name) : CoreM Bool

Equations

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

def Lean.Elab.Command.elabSimprocPattern : CommandElab

Equations

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

def Lean.Elab.Command.elabSimprocPatternBuiltin : CommandElab

Equations

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