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.

Equations

• Lean.Meta.Sym.getBuiltinInstance? type = Lean.Meta.Sym.builtinInsts✝[type]?

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

Equations

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

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).

Equations

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

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

Equations

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

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

Equations

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

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.

Equations

• Lean.Meta.Sym.synthInstanceAndAssign x type = do let __x ← Lean.Meta.Sym.synthInstance? type match __x with | some val => liftM (Lean.Meta.isDefEq x val) | x => pure false