Documentation

Lean.Meta.Tactic.Grind.Ext

← Copula mathematical handbook

Extensionality theorems support.

source
def Lean.Meta.Grind.instantiateExtTheorem (thm : Ext.ExtTheorem) (e : Expr) :
GoalM Unit
Equations
  • One or more equations did not get rendered due to their size.
Instances For