Documentation

Lean.Compiler.LCNF.PhaseExt

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.DeclExtState :
Type
Equations
    Instances For
      source
      def Lean.Compiler.LCNF.DeclExt :
      Type
      Equations
        Instances For
          source
          instance Lean.Compiler.LCNF.instInhabitedDeclExt :
          Inhabited DeclExt
          Equations
            source
            def Lean.Compiler.LCNF.mkDeclExt (name : Name := by exact decl_name%) :
            IO DeclExt
            Equations
              Instances For
                source
                opaque Lean.Compiler.LCNF.baseExt :
                DeclExt
                source
                opaque Lean.Compiler.LCNF.monoExt :
                DeclExt
                source
                def Lean.Compiler.LCNF.getDeclCore? (env : Environment) (ext : DeclExt) (declName : Name) :
                Option Decl
                Equations
                  Instances For
                    source
                    def Lean.Compiler.LCNF.getBaseDecl? (declName : Name) :
                    CoreM (Option Decl)
                    Equations
                      Instances For
                        source
                        def Lean.Compiler.LCNF.getMonoDecl? (declName : Name) :
                        CoreM (Option Decl)
                        Equations
                          Instances For
                            source
                            def Lean.Compiler.LCNF.saveBaseDeclCore (env : Environment) (decl : Decl) :
                            Environment
                            Equations
                              Instances For
                                source
                                def Lean.Compiler.LCNF.saveMonoDeclCore (env : Environment) (decl : Decl) :
                                Environment
                                Equations
                                  Instances For
                                    source
                                    def Lean.Compiler.LCNF.Decl.saveBase (decl : Decl) :
                                    CoreM Unit
                                    Equations
                                      Instances For
                                        source
                                        def Lean.Compiler.LCNF.Decl.saveMono (decl : Decl) :
                                        CoreM Unit
                                        Equations
                                          Instances For
                                            source
                                            def Lean.Compiler.LCNF.Decl.save (decl : Decl) :
                                            CompilerM Unit
                                            Equations
                                              Instances For
                                                source
                                                def Lean.Compiler.LCNF.getDeclAt? (declName : Name) (phase : Phase) :
                                                CoreM (Option Decl)
                                                Equations
                                                  Instances For
                                                    source
                                                    def Lean.Compiler.LCNF.getDecl? (declName : Name) :
                                                    CompilerM (Option Decl)
                                                    Equations
                                                      Instances For
                                                        source
                                                        def Lean.Compiler.LCNF.getExt (phase : Phase) :
                                                        DeclExt
                                                        Equations
                                                          Instances For
                                                            source
                                                            def Lean.Compiler.LCNF.forEachDecl (f : Decl → CoreM Unit) (phase : Phase := Phase.base) :
                                                            CoreM Unit
                                                            Equations
                                                              Instances For
                                                                source
                                                                def Lean.Compiler.LCNF.forEachModuleDecl (moduleName : Name) (f : Decl → CoreM Unit) (phase : Phase := Phase.base) :
                                                                CoreM Unit
                                                                Equations
                                                                  Instances For
                                                                    source
                                                                    def Lean.Compiler.LCNF.forEachMainModuleDecl (f : Decl → CoreM Unit) (phase : Phase := Phase.base) :
                                                                    CoreM Unit
                                                                    Equations
                                                                      Instances For