def Lean.Meta.Grind.getEqcLambdas (root : ENode) : GoalM (Array Expr)

Returns all lambda expressions in the equivalence class with root root.

Equations

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

def Lean.Meta.Grind.getFnRoots (e : Expr) : GoalM (Array Expr)

Returns the root of the functions in the equivalence class containing e. That is, if f a is in roots equivalence class, results contains the root of f.

Equations

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

def Lean.Meta.Grind.propagateBetaEqs (lams : Array Expr) (f : Expr) (args : Array Expr) : GoalM Unit

For each lam in lams s.t. lam and f are in the same equivalence class, propagate f args = lam args.

Equations

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

def Lean.Meta.Grind.propagateBetaForNewApp (e : Expr) : GoalM Unit

Applies beta-reduction for lambdas in fs equivalence class. We use this function while internalizing new applications.

Equations

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