Documentation

Init.System.IO

Like https://hackage.haskell.org/package/ghc-Prim-0.5.2.0/docs/GHC-Prim.html#t:RealWorld. Makes sure we never reorder IO operations.

TODO: mark opaque

Equations
Instances For
    def EIO (ε : Type) :
    Equations
    Instances For
      instance instMonadEIO {ε : Type} :
      Monad (EIO ε)
      Equations
      Equations
      instance instMonadExceptOfEIO {ε : Type} :
      Equations
      instance instOrElseEIO {ε : Type} {α : Type} :
      OrElse (EIO ε α)
      Equations
      • instOrElseEIO = { orElse := MonadExcept.orElse }
      instance instInhabitedEIO {ε : Type} {α : Type} [Inhabited ε] :
      Inhabited (EIO ε α)
      Equations
      def BaseIO :

      An EIO monad that cannot throw exceptions.

      Equations
      Instances For
        @[inline]
        def BaseIO.toEIO {α : Type} {ε : Type} (act : BaseIO α) :
        EIO ε α
        Equations
        Instances For
          Equations
          • instMonadLiftBaseIOEIO = { monadLift := fun {α : Type} => BaseIO.toEIO }
          @[inline]
          def EIO.toBaseIO {ε : Type} {α : Type} (act : EIO ε α) :
          BaseIO (Except ε α)
          Equations
          Instances For
            @[inline]
            def EIO.catchExceptions {ε : Type} {α : Type} (act : EIO ε α) (h : εBaseIO α) :
            Equations
            Instances For
              @[reducible, inline]
              abbrev IO :
              Equations
              Instances For
                @[inline]
                def BaseIO.toIO {α : Type} (act : BaseIO α) :
                IO α
                Equations
                Instances For
                  @[inline]
                  def EIO.toIO {ε : Type} {α : Type} (f : εIO.Error) (act : EIO ε α) :
                  IO α
                  Equations
                  Instances For
                    @[inline]
                    def EIO.toIO' {ε : Type} {α : Type} (act : EIO ε α) :
                    IO (Except ε α)
                    Equations
                    • act.toIO' = liftM act.toBaseIO
                    Instances For
                      @[inline]
                      def IO.toEIO {ε : Type} {α : Type} (f : IO.Errorε) (act : IO α) :
                      EIO ε α
                      Equations
                      Instances For
                        @[inline]
                        unsafe def unsafeBaseIO {α : Type} (fn : BaseIO α) :
                        α
                        Equations
                        Instances For
                          @[inline]
                          unsafe def unsafeEIO {ε : Type} {α : Type} (fn : EIO ε α) :
                          Except ε α
                          Equations
                          Instances For
                            @[inline]
                            unsafe def unsafeIO {α : Type} (fn : IO α) :
                            Equations
                            Instances For
                              @[extern lean_io_timeit]
                              opaque timeit {α : Type} (msg : String) (fn : IO α) :
                              IO α
                              @[extern lean_io_allocprof]
                              opaque allocprof {α : Type} (msg : String) (fn : IO α) :
                              IO α
                              @[extern lean_io_initializing]

                              Programs can execute IO actions during initialization that occurs before the main function is executed. The attribute [init <action>] specifies which IO action is executed to set the value of an opaque constant.

                              The action initializing returns true iff it is invoked during initialization.

                              @[extern lean_io_as_task]

                              Run act in a separate Task. This is similar to Haskell's unsafeInterleaveIO, except that the Task is started eagerly as usual. Thus pure accesses to the Task do not influence the impure act computation. Unlike with pure tasks created by Task.spawn, tasks created by this function will be run even if the last reference to the task is dropped. The act should manually check for cancellation via IO.checkCanceled if it wants to react to that.

                              @[extern lean_io_map_task]
                              opaque BaseIO.mapTask {α : Type u_1} {β : Type} (f : αBaseIO β) (t : Task α) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :

                              See BaseIO.asTask.

                              @[extern lean_io_bind_task]
                              opaque BaseIO.bindTask {α : Type u_1} {β : Type} (t : Task α) (f : αBaseIO (Task β)) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :

                              See BaseIO.asTask.

                              def BaseIO.mapTasks {α : Type u_1} {β : Type} (f : List αBaseIO β) (tasks : List (Task α)) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :
                              Equations
                              Instances For
                                def BaseIO.mapTasks.go {α : Type u_1} {β : Type} (f : List αBaseIO β) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :
                                List (Task α)List αBaseIO (Task β)
                                Equations
                                Instances For
                                  @[inline]
                                  def EIO.asTask {ε : Type} {α : Type} (act : EIO ε α) (prio : optParam Task.Priority Task.Priority.default) :
                                  BaseIO (Task (Except ε α))

                                  EIO specialization of BaseIO.asTask.

                                  Equations
                                  • act.asTask prio = act.toBaseIO.asTask prio
                                  Instances For
                                    @[inline]
                                    def EIO.mapTask {α : Type u_1} {ε : Type} {β : Type} (f : αEIO ε β) (t : Task α) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :
                                    BaseIO (Task (Except ε β))

                                    EIO specialization of BaseIO.mapTask.

                                    Equations
                                    Instances For
                                      @[inline]
                                      def EIO.bindTask {α : Type u_1} {ε : Type} {β : Type} (t : Task α) (f : αEIO ε (Task (Except ε β))) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :
                                      BaseIO (Task (Except ε β))

                                      EIO specialization of BaseIO.bindTask.

                                      Equations
                                      Instances For
                                        @[inline]
                                        def EIO.mapTasks {α : Type u_1} {ε : Type} {β : Type} (f : List αEIO ε β) (tasks : List (Task α)) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :
                                        BaseIO (Task (Except ε β))

                                        EIO specialization of BaseIO.mapTasks.

                                        Equations
                                        Instances For
                                          def IO.ofExcept {ε : Type u_1} {α : Type} [ToString ε] (e : Except ε α) :
                                          IO α
                                          Equations
                                          Instances For
                                            def IO.lazyPure {α : Type} (fn : Unitα) :
                                            IO α
                                            Equations
                                            Instances For
                                              @[extern lean_io_mono_ms_now]

                                              Monotonically increasing time since an unspecified past point in milliseconds. No relation to wall clock time.

                                              @[extern lean_io_mono_nanos_now]

                                              Monotonically increasing time since an unspecified past point in nanoseconds. No relation to wall clock time.

                                              @[extern lean_io_get_random_bytes]
                                              opaque IO.getRandomBytes (nBytes : USize) :

                                              Read bytes from a system entropy source. Not guaranteed to be cryptographically secure. If nBytes = 0, return immediately with an empty buffer.

                                              Equations
                                              Instances For
                                                @[inline]

                                                IO specialization of EIO.asTask.

                                                Equations
                                                Instances For
                                                  @[inline]
                                                  def IO.mapTask {α : Type u_1} {β : Type} (f : αIO β) (t : Task α) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :

                                                  IO specialization of EIO.mapTask.

                                                  Equations
                                                  Instances For
                                                    @[inline]
                                                    def IO.bindTask {α : Type u_1} {β : Type} (t : Task α) (f : αIO (Task (Except IO.Error β))) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :

                                                    IO specialization of EIO.bindTask.

                                                    Equations
                                                    Instances For
                                                      @[inline]
                                                      def IO.mapTasks {α : Type u_1} {β : Type} (f : List αIO β) (tasks : List (Task α)) (prio : optParam Task.Priority Task.Priority.default) (sync : optParam Bool false) :

                                                      IO specialization of EIO.mapTasks.

                                                      Equations
                                                      Instances For
                                                        @[extern lean_io_check_canceled]

                                                        Check if the task's cancellation flag has been set by calling IO.cancel or dropping the last reference to the task.

                                                        @[extern lean_io_cancel]
                                                        opaque IO.cancel {α : Type u_1} :

                                                        Request cooperative cancellation of the task. The task must explicitly call IO.checkCanceled to react to the cancellation.

                                                        inductive IO.TaskState :

                                                        The current state of a Task in the Lean runtime's task manager.

                                                        • waiting: IO.TaskState

                                                          The Task is waiting to be run. It can be waiting for dependencies to complete or sitting in the task manager queue waiting for a thread to run on.

                                                        • running: IO.TaskState

                                                          The Task is actively running on a thread or, in the case of a Promise, waiting for a call to IO.Promise.resolve.

                                                        • finished: IO.TaskState

                                                          The Task has finished running and its result is available. Calling Task.get or IO.wait on the task will not block.

                                                        Instances For
                                                          Equations
                                                          Equations
                                                          Instances For
                                                            @[extern lean_io_get_task_state]
                                                            opaque IO.getTaskState {α : Type u_1} :

                                                            Returns current state of the Task in the Lean runtime's task manager.

                                                            @[inline]
                                                            def IO.hasFinished {α : Type u_1} (task : Task α) :

                                                            Check if the task has finished execution, at which point calling Task.get will return immediately.

                                                            Equations
                                                            Instances For
                                                              @[extern lean_io_wait]
                                                              opaque IO.wait {α : Type} (t : Task α) :

                                                              Wait for the task to finish, then return its result.

                                                              @[extern lean_io_wait_any]
                                                              opaque IO.waitAny {α : Type} (tasks : List (Task α)) (h : autoParam (tasks.length > 0) _auto✝) :

                                                              Wait until any of the tasks in the given list has finished, then return its result.

                                                              @[extern lean_io_get_num_heartbeats]

                                                              Helper method for implementing "deterministic" timeouts. It is the number of "small" memory allocations performed by the current execution thread.

                                                              @[extern lean_io_add_heartbeats]

                                                              Adjusts the heartbeat counter of the current thread by the given amount. This can be useful to give allocation-avoiding code additional "weight" and is also used to adjust the counter after resuming from a snapshot.

                                                              inductive IO.FS.Mode :

                                                              The mode of a file handle (i.e., a set of open flags and an fdopen mode).

                                                              All modes do not translate line endings (i.e., O_BINARY on Windows) and are not inherited across process creation (i.e., O_NOINHERIT on Windows, O_CLOEXEC elsewhere).

                                                              References:

                                                              • read: IO.FS.Mode

                                                                File opened for reading. On open, the stream is positioned at the beginning of the file. Errors if the file does not exist.

                                                                • open flags: O_RDONLY
                                                                • fdopen mode: r
                                                              • write: IO.FS.Mode

                                                                File opened for writing. On open, truncate an existing file to zero length or create a new file. The stream is positioned at the beginning of the file.

                                                                • open flags: O_WRONLY | O_CREAT | O_TRUNC
                                                                • fdopen mode: w
                                                              • writeNew: IO.FS.Mode

                                                                New file opened for writing. On open, create a new file with the stream positioned at the start. Errors if the file already exists.

                                                                • open flags: O_WRONLY | O_CREAT | O_TRUNC | O_EXCL
                                                                • fdopen mode: w
                                                              • readWrite: IO.FS.Mode

                                                                File opened for reading and writing. On open, the stream is positioned at the beginning of the file. Errors if the file does not exist.

                                                                • open flags: O_RDWR
                                                                • fdopen mode: r+
                                                              • append: IO.FS.Mode

                                                                File opened for writing. On open, create a new file if it does not exist. The stream is positioned at the end of the file.

                                                                • open flags: O_WRONLY | O_CREAT | O_APPEND
                                                                • fdopen mode: a
                                                              Instances For
                                                                structure IO.FS.Stream :

                                                                A pure-Lean abstraction of POSIX streams. We use Streams for the standard streams stdin/stdout/stderr so we can capture output of #eval commands into memory.

                                                                • flush : IO Unit
                                                                • read : USizeIO ByteArray

                                                                  Read up to the given number of bytes from the stream. If the returned array is empty, an end-of-file marker has been reached. Note that EOF does not actually close a stream, so further reads may block and return more data.

                                                                • write : ByteArrayIO Unit
                                                                • getLine : IO String

                                                                  Read text up to (including) the next line break from the stream. If the returned string is empty, an end-of-file marker has been reached. Note that EOF does not actually close a stream, so further reads may block and return more data.

                                                                • putStr : StringIO Unit
                                                                • isTty : BaseIO Bool

                                                                  Returns true if a stream refers to a Windows console or Unix terminal.

                                                                Instances For
                                                                  Equations
                                                                  • IO.FS.instInhabitedStream = { default := { flush := default, read := default, write := default, getLine := default, putStr := default, isTty := default } }
                                                                  @[extern lean_get_stdin]
                                                                  @[extern lean_get_stdout]
                                                                  @[extern lean_get_stderr]
                                                                  @[extern lean_get_set_stdin]

                                                                  Replaces the stdin stream of the current thread and returns its previous value.

                                                                  @[extern lean_get_set_stdout]

                                                                  Replaces the stdout stream of the current thread and returns its previous value.

                                                                  @[extern lean_get_set_stderr]

                                                                  Replaces the stderr stream of the current thread and returns its previous value.

                                                                  @[specialize #[]]
                                                                  partial def IO.iterate {α : Type} {β : Type} (a : α) (f : αIO (α β)) :
                                                                  IO β
                                                                  @[extern lean_io_prim_handle_mk]
                                                                  @[extern lean_io_prim_handle_lock]
                                                                  opaque IO.FS.Handle.lock (h : IO.FS.Handle) (exclusive : optParam Bool true) :

                                                                  Acquires an exclusive or shared lock on the handle. Will block to wait for the lock if necessary.

                                                                  NOTE: Acquiring a exclusive lock while already possessing a shared lock will NOT reliably succeed (i.e., it works on Unix but not on Windows).

                                                                  @[extern lean_io_prim_handle_try_lock]

                                                                  Tries to acquire an exclusive or shared lock on the handle. Will NOT block for the lock, but instead return false.

                                                                  NOTE: Acquiring a exclusive lock while already possessing a shared lock will NOT reliably succeed (i.e., it works on Unix but not on Windows).

                                                                  @[extern lean_io_prim_handle_unlock]

                                                                  Releases any previously acquired lock on the handle. Will succeed even if no lock has been acquired.

                                                                  @[extern lean_io_prim_handle_is_tty]

                                                                  Returns true if a handle refers to a Windows console or Unix terminal.

                                                                  @[extern lean_io_prim_handle_flush]
                                                                  @[extern lean_io_prim_handle_rewind]

                                                                  Rewinds the read/write cursor to the beginning of the handle.

                                                                  @[extern lean_io_prim_handle_truncate]

                                                                  Truncates the handle to the read/write cursor.

                                                                  Does not automatically flush. Usually this is fine because the read/write cursor includes buffered writes. However, the combination of buffered writes, then rewind, then truncate, then close may lead to a file with content. If unsure, flush before truncating.

                                                                  @[extern lean_io_prim_handle_read]

                                                                  Read up to the given number of bytes from the handle. If the returned array is empty, an end-of-file marker has been reached. Note that EOF does not actually close a handle, so further reads may block and return more data.

                                                                  @[extern lean_io_prim_handle_write]
                                                                  @[extern lean_io_prim_handle_get_line]

                                                                  Read text up to (including) the next line break from the handle. If the returned string is empty, an end-of-file marker has been reached. Note that EOF does not actually close a handle, so further reads may block and return more data.

                                                                  @[extern lean_io_prim_handle_put_str]
                                                                  @[extern lean_io_realpath]
                                                                  @[extern lean_io_remove_file]
                                                                  @[extern lean_io_remove_dir]

                                                                  Remove given directory. Fails if not empty; see also IO.FS.removeDirAll.

                                                                  @[extern lean_io_create_dir]
                                                                  @[extern lean_io_rename]

                                                                  Moves a file or directory old to the new location new.

                                                                  This function coincides with the POSIX rename function, see there for more information.

                                                                  @[extern lean_io_getenv]
                                                                  opaque IO.getEnv (var : String) :
                                                                  @[extern lean_io_app_path]
                                                                  @[extern lean_io_current_dir]
                                                                  @[inline]
                                                                  def IO.FS.withFile {α : Type} (fn : Lake.FilePath) (mode : IO.FS.Mode) (f : IO.FS.HandleIO α) :
                                                                  IO α
                                                                  Equations
                                                                  Instances For
                                                                    Equations
                                                                    • h.putStrLn s = h.putStr (s.push '\n')
                                                                    Instances For
                                                                      Equations
                                                                      Instances For
                                                                        Equations
                                                                        Instances For
                                                                          Equations
                                                                          Instances For
                                                                            Equations
                                                                            Instances For
                                                                              def IO.FS.writeBinFile (fname : Lake.FilePath) (content : ByteArray) :
                                                                              Equations
                                                                              Instances For
                                                                                def IO.FS.writeFile (fname : Lake.FilePath) (content : String) :
                                                                                Equations
                                                                                Instances For
                                                                                  Equations
                                                                                  • strm.putStrLn s = strm.putStr (s.push '\n')
                                                                                  Instances For
                                                                                    structure IO.FS.DirEntry :
                                                                                    Instances For
                                                                                      Equations
                                                                                      • entry.path = entry.root / { toString := entry.fileName }
                                                                                      Instances For
                                                                                        Instances For
                                                                                          Equations
                                                                                          structure IO.FS.Metadata :
                                                                                          Instances For
                                                                                            @[extern lean_io_read_dir]
                                                                                            @[extern lean_io_metadata]
                                                                                            Equations
                                                                                            Instances For
                                                                                              Equations
                                                                                              Instances For

                                                                                                Return all filesystem entries of a preorder traversal of all directories satisfying enter, starting at p. Symbolic links are visited as well by default.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  def IO.withStdin {m : TypeType u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : IO.FS.Stream) (x : m α) :
                                                                                                  m α
                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    def IO.withStdout {m : TypeType u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : IO.FS.Stream) (x : m α) :
                                                                                                    m α
                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      def IO.withStderr {m : TypeType u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (h : IO.FS.Stream) (x : m α) :
                                                                                                      m α
                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        def IO.print {α : Type u_1} [ToString α] (s : α) :
                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          def IO.println {α : Type u_1} [ToString α] (s : α) :
                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            def IO.eprint {α : Type u_1} [ToString α] (s : α) :
                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              def IO.eprintln {α : Type u_1} [ToString α] (s : α) :
                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                Equations
                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                Instances For

                                                                                                                  Create given path and all missing parents as directories.

                                                                                                                  Fully remove given directory by deleting all contained files and directories in an unspecified order. Fails if any contained entry cannot be deleted or was newly created during execution.

                                                                                                                  @[extern lean_io_process_get_current_dir]

                                                                                                                  Returns the current working directory of the calling process.

                                                                                                                  @[extern lean_io_process_set_current_dir]

                                                                                                                  Sets the current working directory of the calling process.

                                                                                                                  @[extern lean_io_process_get_pid]

                                                                                                                  Returns the process ID of the calling process.

                                                                                                                  Instances For
                                                                                                                    Instances For
                                                                                                                      • stdin : cfg.stdin.toHandleType
                                                                                                                      • stdout : cfg.stdout.toHandleType
                                                                                                                      • stderr : cfg.stderr.toHandleType
                                                                                                                      Instances For
                                                                                                                        @[extern lean_io_process_spawn]
                                                                                                                        opaque IO.Process.spawn (args : IO.Process.SpawnArgs) :
                                                                                                                        IO (IO.Process.Child args.toStdioConfig)
                                                                                                                        @[extern lean_io_process_child_wait]
                                                                                                                        @[extern lean_io_process_child_kill]

                                                                                                                        Terminates the child process using the SIGTERM signal or a platform analogue. If the process was started using SpawnArgs.setsid, terminates the entire process group instead.

                                                                                                                        @[extern lean_io_process_child_take_stdin]
                                                                                                                        opaque IO.Process.Child.takeStdin {cfg : IO.Process.StdioConfig} :
                                                                                                                        IO.Process.Child cfgIO (cfg.stdin.toHandleType × IO.Process.Child { stdin := IO.Process.Stdio.null, stdout := cfg.stdout, stderr := cfg.stderr })

                                                                                                                        Extract the stdin field from a Child object, allowing them to be freed independently. This operation is necessary for closing the child process' stdin while still holding on to a process handle, e.g. for Child.wait. A file handle is closed when all references to it are dropped, which without this operation includes the Child object.

                                                                                                                        Instances For

                                                                                                                          Run process to completion and capture output. The process does not inherit the standard input of the caller.

                                                                                                                          Equations
                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                          Instances For

                                                                                                                            Run process to completion and return stdout on success.

                                                                                                                            Equations
                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                            Instances For
                                                                                                                              @[extern lean_io_exit]
                                                                                                                              opaque IO.Process.exit {α : Type} :
                                                                                                                              UInt8IO α
                                                                                                                              structure IO.AccessRight :
                                                                                                                              Instances For
                                                                                                                                Equations
                                                                                                                                • acc.flags = let r := if acc.read = true then 4 else 0; let w := if acc.write = true then 2 else 0; let x := if acc.execution = true then 1 else 0; r.lor (w.lor x)
                                                                                                                                Instances For
                                                                                                                                  structure IO.FileRight :
                                                                                                                                  Instances For
                                                                                                                                    Equations
                                                                                                                                    • acc.flags = let u := acc.user.flags.shiftLeft 6; let g := acc.group.flags.shiftLeft 3; let o := acc.other.flags; u.lor (g.lor o)
                                                                                                                                    Instances For
                                                                                                                                      @[extern lean_chmod]
                                                                                                                                      opaque IO.Prim.setAccessRights (filename : Lake.FilePath) (mode : UInt32) :
                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        @[reducible, inline]
                                                                                                                                        abbrev IO.Ref (α : Type) :

                                                                                                                                        References

                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          def IO.mkRef {α : Type} (a : α) :
                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            structure IO.CancelToken :

                                                                                                                                            Mutable cell that can be passed around for purposes of cooperative task cancellation: request cancellation with CancelToken.set and check for it with CancelToken.isSet.

                                                                                                                                            This is a more flexible alternative to Task.cancel as the token can be shared between multiple tasks.

                                                                                                                                            Instances For

                                                                                                                                              Creates a new cancellation token.

                                                                                                                                              Equations
                                                                                                                                              Instances For

                                                                                                                                                Activates a cancellation token. Idempotent.

                                                                                                                                                Equations
                                                                                                                                                Instances For

                                                                                                                                                  Checks whether the cancellation token has been activated.

                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    @[export lean_stream_of_handle]
                                                                                                                                                    Equations
                                                                                                                                                    • IO.FS.Stream.ofHandle h = { flush := h.flush, read := h.read, write := h.write, getLine := h.getLine, putStr := h.putStr, isTty := h.isTty }
                                                                                                                                                    Instances For
                                                                                                                                                      Instances For
                                                                                                                                                        Equations
                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                        Instances For
                                                                                                                                                          def IO.FS.withIsolatedStreams {m : TypeType u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (x : m α) (isolateStderr : optParam Bool true) :
                                                                                                                                                          m (String × α)

                                                                                                                                                          Run action with stdin emptied and stdout+stderr captured into a String.

                                                                                                                                                          Equations
                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                          Instances For
                                                                                                                                                            class Lean.Eval (α : Type u) :

                                                                                                                                                            Typeclass used for presenting the output of an #eval command.

                                                                                                                                                            Instances
                                                                                                                                                              instance Lean.instEval {α : Type u_1} [ToString α] :
                                                                                                                                                              Equations
                                                                                                                                                              instance Lean.instEvalOfRepr {α : Type u_1} [Repr α] :
                                                                                                                                                              Equations
                                                                                                                                                              Equations
                                                                                                                                                              instance Lean.instEvalIO {α : Type} [Lean.Eval α] :
                                                                                                                                                              Equations
                                                                                                                                                              Equations
                                                                                                                                                              Equations
                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                              Instances For