Documentation

Lean.Meta.Sym.SynthInstance

source
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
Instances For
    source
    def Lean.Meta.Sym.synthInstanceMeta? (type : Expr) :
    MetaM (Option Expr)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[reducible, inline]
      abbrev Lean.Meta.Sym.synthInstance? (type : Expr) :
      SymM (Option Expr)
      Equations
      Instances For
        source
        def Lean.Meta.Sym.synthInstance (type : Expr) :
        SymM Expr
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          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
          Instances For