Documentation

Lean.Compiler.LCNF.PhaseExt

source
@[inline, reducible]
abbrev Lean.Compiler.LCNF.DeclExtState :
Type
Instances For
    source
    @[inline, reducible]
    abbrev Lean.Compiler.LCNF.DeclExt :
    Type
    Instances For
      source
      def Lean.Compiler.LCNF.mkDeclExt (name : autoParam Lake.Name _auto✝) :
      IO Lean.Compiler.LCNF.DeclExt
      Instances For
        source
        opaque Lean.Compiler.LCNF.baseExt :
        Lean.PersistentEnvExtension Lean.Compiler.LCNF.Decl Lean.Compiler.LCNF.Decl Lean.Compiler.LCNF.DeclExtState
        source
        opaque Lean.Compiler.LCNF.monoExt :
        Lean.PersistentEnvExtension Lean.Compiler.LCNF.Decl Lean.Compiler.LCNF.Decl Lean.Compiler.LCNF.DeclExtState
        source
        def Lean.Compiler.LCNF.getDeclCore? (env : Lean.Environment) (ext : Lean.Compiler.LCNF.DeclExt) (declName : Lake.Name) :
        Option Lean.Compiler.LCNF.Decl
        Instances For
          source
          def Lean.Compiler.LCNF.getBaseDecl? (declName : Lake.Name) :
          Lean.CoreM (Option Lean.Compiler.LCNF.Decl)
          Instances For
            source
            def Lean.Compiler.LCNF.getMonoDecl? (declName : Lake.Name) :
            Lean.CoreM (Option Lean.Compiler.LCNF.Decl)
            Instances For
              source
              def Lean.Compiler.LCNF.saveBaseDeclCore (env : Lean.Environment) (decl : Lean.Compiler.LCNF.Decl) :
              Lean.Environment
              Instances For
                source
                def Lean.Compiler.LCNF.saveMonoDeclCore (env : Lean.Environment) (decl : Lean.Compiler.LCNF.Decl) :
                Lean.Environment
                Instances For
                  source
                  def Lean.Compiler.LCNF.Decl.saveBase (decl : Lean.Compiler.LCNF.Decl) :
                  Lean.CoreM Unit
                  Instances For
                    source
                    def Lean.Compiler.LCNF.Decl.saveMono (decl : Lean.Compiler.LCNF.Decl) :
                    Lean.CoreM Unit
                    Instances For
                      source
                      def Lean.Compiler.LCNF.Decl.save (decl : Lean.Compiler.LCNF.Decl) :
                      Lean.Compiler.LCNF.CompilerM Unit
                      Instances For
                        source
                        def Lean.Compiler.LCNF.getDeclAt? (declName : Lake.Name) (phase : Lean.Compiler.LCNF.Phase) :
                        Lean.CoreM (Option Lean.Compiler.LCNF.Decl)
                        Instances For
                          source
                          def Lean.Compiler.LCNF.getDecl? (declName : Lake.Name) :
                          Lean.Compiler.LCNF.CompilerM (Option Lean.Compiler.LCNF.Decl)
                          Instances For
                            source
                            def Lean.Compiler.LCNF.getExt (phase : Lean.Compiler.LCNF.Phase) :
                            Lean.Compiler.LCNF.DeclExt
                            Instances For
                              source
                              def Lean.Compiler.LCNF.forEachDecl (f : Lean.Compiler.LCNF.Decl → Lean.CoreM Unit) (phase : optParam Lean.Compiler.LCNF.Phase Lean.Compiler.LCNF.Phase.base) :
                              Lean.CoreM Unit
                              Instances For
                                source
                                def Lean.Compiler.LCNF.forEachModuleDecl (moduleName : Lake.Name) (f : Lean.Compiler.LCNF.Decl → Lean.CoreM Unit) (phase : optParam Lean.Compiler.LCNF.Phase Lean.Compiler.LCNF.Phase.base) :
                                Lean.CoreM Unit
                                Instances For
                                  source
                                  def Lean.Compiler.LCNF.forEachMainModuleDecl (f : Lean.Compiler.LCNF.Decl → Lean.CoreM Unit) (phase : optParam Lean.Compiler.LCNF.Phase Lean.Compiler.LCNF.Phase.base) :
                                  Lean.CoreM Unit
                                  Instances For