def Lean.Meta.Sym.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.Sym.synthInstanceMeta? (type : Expr) : MetaM (Option Expr)

def Lean.Meta.Sym.registerInstance (type inst : Expr) : SymM Unit

Registers inst as the instance for type. synthInstance? returns it without running typeclass resolution, making inst the canonical representative for type. Intended for satellite modules that construct instances for types they create themselves (e.g., grind linarith's envelope type IntModule.OfNatModule.Q).

def Lean.Meta.Sym.synthInstance? (type : Expr) : SymM (Option Expr)

def Lean.Meta.Sym.synthInstance (type : Expr) : SymM Expr

def Lean.Meta.Sym.synthInstanceAndAssign (x type : Expr) : SymM Bool

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