def Lean.Meta.Grind.getBuiltinInstance? (type : Expr) : Option Expr

Some modules in grind use builtin instances defined directly in core (e.g., lia). Users may provide nonstandard instances that are definitionally equal to the ones in core. Given a type, such as HAdd Int Int Int, this function returns the instance defined in core.

def Lean.Meta.Grind.synthInstanceMeta? (type : Expr) : MetaM (Option Expr)

@[reducible, inline]

abbrev Lean.Meta.Grind.synthInstance? (type : Expr) : GoalM (Option Expr)

def Lean.Meta.Grind.synthInstance (type : Expr) : GoalM Expr

def Lean.Meta.Grind.synthInstanceAndAssign (x type : Expr) : GoalM Bool

Helper function for instantiating a type class type, and then using the result to perform isDefEq x val.