Documentation

Lean.Meta.Tactic.Grind.Ext

Extensionality theorems support.

source
def Lean.Meta.Grind.instantiateExtTheorem (thm : Ext.ExtTheorem) (e : Expr) :
GoalM Unit
Equations
    Instances For