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

Equations

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

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.synthInstance? type = liftM (Lean.Meta.Grind.synthInstanceMeta? type)

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

Equations

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

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.

Equations

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