Documentation

Lean.Meta.Tactic.Grind.AC.Internalize

source
partial def Lean.Meta.Grind.AC.reify (e : Expr) :
ACM Grind.AC.Expr
source
def Lean.Meta.Grind.AC.internalize (e : Expr) (parent? : Option Expr) :
GoalM Unit
Equations
  • One or more equations did not get rendered due to their size.
Instances For