Documentation

Lean.Compiler.LCNF.ExtractClosed

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.ExtractClosed.ExtractM (α : Type) :
Type
Equations
    Instances For
      source
      partial def Lean.Compiler.LCNF.ExtractClosed.extractLetValue (v : LetValue) :
      ExtractM Unit
      source
      partial def Lean.Compiler.LCNF.ExtractClosed.extractArg (arg : Arg) :
      ExtractM Unit
      source
      partial def Lean.Compiler.LCNF.ExtractClosed.extractFVar (fvarId : FVarId) :
      ExtractM Unit
      source
      def Lean.Compiler.LCNF.ExtractClosed.isIrrelevantArg (arg : Arg) :
      Bool
      Equations
        Instances For
          source
          structure Lean.Compiler.LCNF.ExtractClosed.Context :
          Type
          Instances For
            source
            structure Lean.Compiler.LCNF.ExtractClosed.State :
            Type
            Instances For
              source
              @[reducible, inline]
              abbrev Lean.Compiler.LCNF.ExtractClosed.M (α : Type) :
              Type
              Equations
                Instances For
                  source
                  partial def Lean.Compiler.LCNF.ExtractClosed.shouldExtractLetValue (isRoot : Bool) (v : LetValue) :
                  M Bool
                  source
                  partial def Lean.Compiler.LCNF.ExtractClosed.shouldExtractArg (arg : Arg) :
                  M Bool
                  source
                  partial def Lean.Compiler.LCNF.ExtractClosed.shouldExtractFVar (fvarId : FVarId) :
                  M Bool
                  source
                  partial def Lean.Compiler.LCNF.ExtractClosed.visitCode (code : Code) :
                  M Code
                  source
                  def Lean.Compiler.LCNF.ExtractClosed.visitDecl (decl : Decl) :
                  M Decl
                  Equations
                    Instances For
                      source
                      def Lean.Compiler.LCNF.Decl.extractClosed (decl : Decl) (sccDecls : Array Decl) :
                      CompilerM (Array Decl)
                      Equations
                        Instances For
                          source
                          def Lean.Compiler.LCNF.extractClosed :
                          Pass
                          Equations
                            Instances For