Create a new local function declaration when info.args.size < info.params.size. We use this function to inline/specialize a partial application of a local function.

Instances For

    When the configuration flag etaPoly = true, we eta-expand partial applications of functions that take local instances as arguments. This kind of function is inlined or specialized, and we create new simplification opportunities by eta-expanding them.

    Instances For

      Similar to Code.isReturnOf, but taking the current substitution into account.

      Instances For

        If the value of the given let-declaration is an application that can be inlined, inline it and simplify the result.

        k is the "continuation" for the let declaration, if the application is inlined, it will also be simplified.

        Note: inlineApp? did not use to be in this mutually recursive declaration. It used to be invoked by simp, and would return Option Code that would be then simplified by simp. However, this simpler architecture produced an exponential blowup in when processing functions such as Lean.Elab.Deriving.Ord.mkMatch.mkAlts. The key problem is that when inlining a declaration we often can reduce the number of exit points by simplified the inlined code, and then connecting the result to the continuation k. However, this optimization is only possible if we simplify the inlined code before we attach it to the continuation.