Documentation

Lean.Compiler.LCNF.PullLetDecls

source
structure Lean.Compiler.LCNF.PullLetDecls.Context :
Type
Instances For
    source
    structure Lean.Compiler.LCNF.PullLetDecls.State :
    Type
    Instances For
      source
      @[inline, reducible]
      abbrev Lean.Compiler.LCNF.PullLetDecls.PullM (α : Type) :
      Type
      Instances For
        source
        @[inline]
        def Lean.Compiler.LCNF.PullLetDecls.withFVar {α : Type} (fvarId : Lean.FVarId) (x : Lean.Compiler.LCNF.PullLetDecls.PullM α) :
        Lean.Compiler.LCNF.PullLetDecls.PullM α
        Instances For
          source
          @[inline]
          def Lean.Compiler.LCNF.PullLetDecls.withParams {α : Type} (ps : Array Lean.Compiler.LCNF.Param) (x : Lean.Compiler.LCNF.PullLetDecls.PullM α) :
          Lean.Compiler.LCNF.PullLetDecls.PullM α
          Instances For
            source
            @[inline]
            def Lean.Compiler.LCNF.PullLetDecls.withNewScope {α : Type} (x : Lean.Compiler.LCNF.PullLetDecls.PullM α) :
            Lean.Compiler.LCNF.PullLetDecls.PullM α
            Instances For
              source
              def Lean.Compiler.LCNF.PullLetDecls.withCheckpoint (x : Lean.Compiler.LCNF.PullLetDecls.PullM Lean.Compiler.LCNF.Code) :
              Lean.Compiler.LCNF.PullLetDecls.PullM Lean.Compiler.LCNF.Code
              Instances For
                source
                partial def Lean.Compiler.LCNF.PullLetDecls.withCheckpoint.go (c : Lean.Compiler.LCNF.Code) (toPull : Array Lean.Compiler.LCNF.LetDecl) (i : Nat) (included : Lean.FVarIdSet) :
                StateM (Array Lean.Compiler.LCNF.LetDecl) Lean.Compiler.LCNF.Code
                source
                def Lean.Compiler.LCNF.PullLetDecls.attachToPull (c : Lean.Compiler.LCNF.Code) :
                Lean.Compiler.LCNF.PullLetDecls.PullM Lean.Compiler.LCNF.Code
                Instances For
                  source
                  def Lean.Compiler.LCNF.PullLetDecls.shouldPull (decl : Lean.Compiler.LCNF.LetDecl) :
                  Lean.Compiler.LCNF.PullLetDecls.PullM Bool
                  Instances For
                    source
                    partial def Lean.Compiler.LCNF.PullLetDecls.pullAlt (alt : Lean.Compiler.LCNF.Alt) :
                    Lean.Compiler.LCNF.PullLetDecls.PullM Lean.Compiler.LCNF.Alt
                    source
                    partial def Lean.Compiler.LCNF.PullLetDecls.pullDecls (code : Lean.Compiler.LCNF.Code) :
                    Lean.Compiler.LCNF.PullLetDecls.PullM Lean.Compiler.LCNF.Code
                    source
                    def Lean.Compiler.LCNF.PullLetDecls.PullM.run {α : Type} (x : Lean.Compiler.LCNF.PullLetDecls.PullM α) (isCandidateFn : Lean.Compiler.LCNF.LetDecl → Lean.FVarIdSet → Lean.Compiler.LCNF.CompilerM Bool) :
                    Lean.Compiler.LCNF.CompilerM α
                    Instances For
                      source
                      def Lean.Compiler.LCNF.Decl.pullLetDecls (decl : Lean.Compiler.LCNF.Decl) (isCandidateFn : Lean.Compiler.LCNF.LetDecl → Lean.FVarIdSet → Lean.Compiler.LCNF.CompilerM Bool) :
                      Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Decl
                      Instances For
                        source
                        def Lean.Compiler.LCNF.Decl.pullInstances (decl : Lean.Compiler.LCNF.Decl) :
                        Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Decl
                        Instances For
                          source
                          def Lean.Compiler.LCNF.pullInstances :
                          Lean.Compiler.LCNF.Pass
                          Instances For