Documentation

Lean.Compiler.LCNF.PullFunDecls

Local function declaration and join point being pulled.

Instances For
    @[reducible, inline]

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

    Equations
      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.

        Equations
          Instances For

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

            Equations
              Instances For

                Construct the code fun p.decl k or jp p.decl k.

                Equations
                  Instances For

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

                    Equations
                      Instances For

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

                        Equations
                          Instances For

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

                            Equations
                              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.

                                Equations
                                  Instances For
                                    Equations
                                      Instances For