Documentation

Lean.Elab.Import

@[reducible, inline]
Equations
    Instances For
      Equations
        Instances For
          Equations
            Instances For
              @[reducible, inline]
              Equations
                Instances For
                  def Lean.Elab.processHeaderCore (startPos : String.Pos) (imports : Array Import) (isModule : Bool) (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0) (plugins : Array System.FilePath := #[]) (leakEnv : Bool := false) (mainModule : Name := Name.anonymous) (arts : NameMap ModuleArtifacts := ) :
                  Equations
                    Instances For
                      @[inline]
                      def Lean.Elab.processHeader (header : HeaderSyntax) (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0) (plugins : Array System.FilePath := #[]) (leakEnv : Bool := false) (mainModule : Name := Name.anonymous) :

                      Elaborates the given header syntax into an environment.

                      If mainModule is not given, Environment.setMainModule should be called manually. This is a backwards compatibility measure not compatible with the module system.

                      Equations
                        Instances For
                          Equations
                            Instances For
                              @[export lean_print_imports]
                              def Lean.Elab.printImports (input : String) (fileName : Option String) :
                              Equations
                                Instances For
                                  @[export lean_print_import_srcs]
                                  def Lean.Elab.printImportSrcs (input : String) (fileName : Option String) :
                                  Equations
                                    Instances For