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

Equations

• Lean.Elab.elabSimprocPattern stx = let go := do let pattern ← Lean.Elab.Term.elabTerm stx none Lean.Elab.Term.synthesizeSyntheticMVars pure pattern; go.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.DiscrTree.mkPath pattern Lean.Meta.simpDtConfig

def Lean.Elab.checkSimprocType (declName : Lake.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.