Documentation

Lean.Compiler.LCNF.PullFunDecls

Local function declaration and join point being pulled.

Instances For
    @[inline, reducible]

    The PullM state contains the local function declarations and join points being pulled.

    Instances For

      Extract from the state any local function declarations that depends on the given free variable. The idea is that we have to stop pulling these declarations because they depend on fvarId.

      Instances For

        Similar to findFVarDeps. Extract from the state any local function declarations that depends on the given parameters.

        Instances For

          Attach the given array of local function declarations and join points to k.

          Instances For

            Extract from the state any local function declarations that depends on the given free variable, and attach to code k.

            Instances For

              Similar to attachFVarDeps. Extract from the state any local function declarations that depends on the given parameters, and attach to code k.

              Instances For

                Add local function declaration (or join point if isFun = false) to the state.

                Pull local function declarations and join points in code. The state contains the declarations being pulled.

                Pull local function declarations and join points in the given declaration.

                Instances For