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

Equations

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

def Lean.Elab.mkSimprocPatternFromExpr (e : Expr) : MetaM Meta.Sym.Pattern

Equations

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

def Lean.Elab.elabCbvSimprocKeys (stx : Syntax) : MetaM (Array Meta.DiscrTree.Key)

Equations

• Lean.Elab.elabCbvSimprocKeys stx = do let pattern ← Lean.Elab.elabCbvSimprocPattern stx let symPattern ← Lean.Elab.mkSimprocPatternFromExpr pattern pure symPattern.mkDiscrTreeKeys

def Lean.Elab.checkCbvSimprocType (declName : Name) : CoreM Unit

Equations

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

def Lean.Elab.Command.elabCbvSimprocPattern : CommandElab

Equations

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

def Lean.Elab.Command.elabCbvSimprocPatternBuiltin : CommandElab

Equations

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