Documentation

Lean.Meta.Tactic.Grind.Beta

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

Equations
    Instances For

      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
        Instances For

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

          Equations
            Instances For

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

              Equations
                Instances For