Loogle!

Result

Found 726 declarations mentioning IO. Of these, only the first 200 are shown.

• IO 📋 Init.System.IO
  : Type → Type
• IO.appDir 📋 Init.System.IO
  : IO System.FilePath
• IO.appPath 📋 Init.System.IO
  : IO System.FilePath
• IO.currentDir 📋 Init.System.IO
  : IO System.FilePath
• IO.FS.createTempDir 📋 Init.System.IO
  : IO System.FilePath
• IO.Process.getCurrentDir 📋 Init.System.IO
  : IO System.FilePath
• IO.getRandomBytes 📋 Init.System.IO
  (nBytes : USize) : IO ByteArray
• IO.FS.createDirAll 📋 Init.System.IO
  (p : System.FilePath) : IO Unit
• IO.FS.readBinFile 📋 Init.System.IO
  (fname : System.FilePath) : IO ByteArray
• IO.FS.readFile 📋 Init.System.IO
  (fname : System.FilePath) : IO String
• IO.FS.realPath 📋 Init.System.IO
  (fname : System.FilePath) : IO System.FilePath
• IO.FS.removeDirAll 📋 Init.System.IO
  (p : System.FilePath) : IO Unit
• IO.FS.Handle.readBinToEnd 📋 Init.System.IO
  (h : IO.FS.Handle) : IO ByteArray
• IO.FS.Handle.readToEnd 📋 Init.System.IO
  (h : IO.FS.Handle) : IO String
• IO.FS.Stream.flush 📋 Init.System.IO
  (self : IO.FS.Stream) : IO Unit
• IO.FS.Stream.getLine 📋 Init.System.IO
  (self : IO.FS.Stream) : IO String
• IO.FS.Stream.readBinToEnd 📋 Init.System.IO
  (s : IO.FS.Stream) : IO ByteArray
• IO.FS.Stream.readToEnd 📋 Init.System.IO
  (s : IO.FS.Stream) : IO String
• IO.FS.createDir 📋 Init.System.IO
  : System.FilePath → IO Unit
• IO.FS.removeDir 📋 Init.System.IO
  : System.FilePath → IO Unit
• IO.FS.removeFile 📋 Init.System.IO
  (fname : System.FilePath) : IO Unit
• IO.Process.setCurrentDir 📋 Init.System.IO
  (path : System.FilePath) : IO Unit
• System.FilePath.metadata 📋 Init.System.IO
  : System.FilePath → IO IO.FS.Metadata
• System.FilePath.symlinkMetadata 📋 Init.System.IO
  : System.FilePath → IO IO.FS.Metadata
• IO.FS.Handle.flush 📋 Init.System.IO
  (h : IO.FS.Handle) : IO Unit
• IO.FS.Handle.getLine 📋 Init.System.IO
  (h : IO.FS.Handle) : IO String
• IO.FS.Handle.rewind 📋 Init.System.IO
  (h : IO.FS.Handle) : IO Unit
• IO.FS.Handle.truncate 📋 Init.System.IO
  (h : IO.FS.Handle) : IO Unit
• IO.FS.Handle.unlock 📋 Init.System.IO
  (h : IO.FS.Handle) : IO Unit
• IO.setAccessRights 📋 Init.System.IO
  (filename : System.FilePath) (mode : IO.FileRight) : IO Unit
• IO.FS.createTempFile 📋 Init.System.IO
  : IO (IO.FS.Handle × System.FilePath)
• IO.FS.lines 📋 Init.System.IO
  (fname : System.FilePath) : IO (Array String)
• IO.FS.writeBinFile 📋 Init.System.IO
  (fname : System.FilePath) (content : ByteArray) : IO Unit
• IO.FS.writeFile 📋 Init.System.IO
  (fname : System.FilePath) (content : String) : IO Unit
• IO.Process.exit 📋 Init.System.IO
  {α : Type} : UInt8 → IO α
• IO.Process.forceExit 📋 Init.System.IO
  {α : Type} : UInt8 → IO α
• IO.FS.Handle.lines 📋 Init.System.IO
  (h : IO.FS.Handle) : IO (Array String)
• IO.FS.Handle.putStrLn 📋 Init.System.IO
  (h : IO.FS.Handle) (s : String) : IO Unit
• IO.FS.Handle.readBinToEndInto 📋 Init.System.IO
  (h : IO.FS.Handle) (buf : ByteArray) : IO ByteArray
• IO.FS.Stream.lines 📋 Init.System.IO
  (s : IO.FS.Stream) : IO (Array String)
• IO.FS.Stream.putStr 📋 Init.System.IO
  (self : IO.FS.Stream) : String → IO Unit
• IO.FS.Stream.putStrLn 📋 Init.System.IO
  (strm : IO.FS.Stream) (s : String) : IO Unit
• IO.FS.Stream.read 📋 Init.System.IO
  (self : IO.FS.Stream) : USize → IO ByteArray
• IO.FS.Stream.readBinToEndInto 📋 Init.System.IO
  (s : IO.FS.Stream) (buf : ByteArray) : IO ByteArray
• IO.FS.Stream.write 📋 Init.System.IO
  (self : IO.FS.Stream) : ByteArray → IO Unit
• IO.Prim.setAccessRights 📋 Init.System.IO
  (filename : System.FilePath) (mode : UInt32) : IO Unit
• System.FilePath.readDir 📋 Init.System.IO
  : System.FilePath → IO (Array IO.FS.DirEntry)
• IO.FS.Handle.mk 📋 Init.System.IO
  (fn : System.FilePath) (mode : IO.FS.Mode) : IO IO.FS.Handle
• IO.FS.Handle.read 📋 Init.System.IO
  (h : IO.FS.Handle) (bytes : USize) : IO ByteArray
• BaseIO.toIO 📋 Init.System.IO
  {α : Type} (act : BaseIO α) : IO α
• IO.lazyPure 📋 Init.System.IO
  {α : Type} (fn : Unit → α) : IO α
• IO.FS.hardLink 📋 Init.System.IO
  (orig link : System.FilePath) : IO Unit
• IO.FS.rename 📋 Init.System.IO
  (old new : System.FilePath) : IO Unit
• IO.Process.spawn 📋 Init.System.IO
  (args : IO.Process.SpawnArgs) : IO (IO.Process.Child args.toStdioConfig)
• IO.FS.Handle.putStr 📋 Init.System.IO
  (h : IO.FS.Handle) (s : String) : IO Unit
• IO.FS.Handle.write 📋 Init.System.IO
  (h : IO.FS.Handle) (buffer : ByteArray) : IO Unit
• unsafeIO 📋 Init.System.IO
  {α : Type} (fn : IO α) : Except IO.Error α
• IO.eprint 📋 Init.System.IO
  {α : Type u_1} [ToString α] (s : α) : IO Unit
• IO.eprintln 📋 Init.System.IO
  {α : Type u_1} [ToString α] (s : α) : IO Unit
• IO.print 📋 Init.System.IO
  {α : Type u_1} [ToString α] (s : α) : IO Unit
• IO.println 📋 Init.System.IO
  {α : Type u_1} [ToString α] (s : α) : IO Unit
• IO.Process.Child.kill 📋 Init.System.IO
  {cfg : IO.Process.StdioConfig} : IO.Process.Child cfg → IO Unit
• IO.Process.Child.wait 📋 Init.System.IO
  {cfg : IO.Process.StdioConfig} : IO.Process.Child cfg → IO UInt32
• allocprof 📋 Init.System.IO
  {α : Type} (msg : String) (fn : IO α) : IO α
• timeit 📋 Init.System.IO
  {α : Type} (msg : String) (fn : IO α) : IO α
• IO.FS.Handle.lock 📋 Init.System.IO
  (h : IO.FS.Handle) (exclusive : Bool := true) : IO Unit
• IO.FS.Handle.tryLock 📋 Init.System.IO
  (h : IO.FS.Handle) (exclusive : Bool := true) : IO Bool
• IO.Process.Child.tryWait 📋 Init.System.IO
  {cfg : IO.Process.StdioConfig} : IO.Process.Child cfg → IO (Option UInt32)
• IO.FS.withFile 📋 Init.System.IO
  {α : Type} (fn : System.FilePath) (mode : IO.FS.Mode) (f : IO.FS.Handle → IO α) : IO α
• IO.Process.output 📋 Init.System.IO
  (args : IO.Process.SpawnArgs) (input? : Option String := none) : IO IO.Process.Output
• IO.Process.run 📋 Init.System.IO
  (args : IO.Process.SpawnArgs) (input? : Option String := none) : IO String
• EIO.toIO 📋 Init.System.IO
  {ε α : Type} (f : ε → IO.Error) (act : EIO ε α) : IO α
• EIO.toIO' 📋 Init.System.IO
  {ε α : Type} (act : EIO ε α) : IO (Except ε α)
• IO.ofExcept 📋 Init.System.IO
  {ε : Type u_1} {α : Type} [ToString ε] (e : Except ε α) : IO α
• IO.toEIO 📋 Init.System.IO
  {ε α : Type} (f : IO.Error → ε) (act : IO α) : EIO ε α
• IO.iterate 📋 Init.System.IO
  {α β : Type} (a : α) (f : α → IO (α ⊕ β)) : IO β
• IO.asTask 📋 Init.System.IO
  {α : Type} (act : IO α) (prio : Task.Priority := Task.Priority.default) : BaseIO (Task (Except IO.Error α))
• IO.chainTask 📋 Init.System.IO
  {α : Type u_1} (t : Task α) (f : α → IO Unit) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : IO Unit
• IO.FS.withTempDir 📋 Init.System.IO
  {m : Type → Type u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : System.FilePath → m α) : m α
• IO.Process.Child.takeStdin 📋 Init.System.IO
  {cfg : IO.Process.StdioConfig} : IO.Process.Child cfg → IO (cfg.stdin.toHandleType × IO.Process.Child { stdin := IO.Process.Stdio.null, stdout := cfg.stdout, stderr := cfg.stderr })
• IO.FS.withTempFile 📋 Init.System.IO
  {m : Type → Type u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT IO m] (f : IO.FS.Handle → System.FilePath → m α) : m α
• IO.FS.Stream.mk 📋 Init.System.IO
  (flush : IO Unit) (read : USize → IO ByteArray) (write : ByteArray → IO Unit) (getLine : IO String) (putStr : String → IO Unit) (isTty : BaseIO Bool) : IO.FS.Stream
• IO.mapTask 📋 Init.System.IO
  {α : Type u_1} {β : Type} (f : α → IO β) (t : Task α) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : BaseIO (Task (Except IO.Error β))
• System.FilePath.walkDir 📋 Init.System.IO
  (p : System.FilePath) (enter : System.FilePath → IO Bool := fun x => pure true) : IO (Array System.FilePath)
• IO.mapTasks 📋 Init.System.IO
  {α : Type u_1} {β : Type} (f : List α → IO β) (tasks : List (Task α)) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : BaseIO (Task (Except IO.Error β))
• IO.bindTask 📋 Init.System.IO
  {α : Type u_1} {β : Type} (t : Task α) (f : α → IO (Task (Except IO.Error β))) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : BaseIO (Task (Except IO.Error β))
• IO.FS.Stream.mk.sizeOf_spec 📋 Init.System.IO
  (flush : IO Unit) (read : USize → IO ByteArray) (write : ByteArray → IO Unit) (getLine : IO String) (putStr : String → IO Unit) (isTty : BaseIO Bool) : sizeOf { flush := flush, read := read, write := write, getLine := getLine, putStr := putStr, isTty := isTty } = 1
• IO.FS.Stream.mk.injEq 📋 Init.System.IO
  (flush : IO Unit) (read : USize → IO ByteArray) (write : ByteArray → IO Unit) (getLine : IO String) (putStr : String → IO Unit) (isTty : BaseIO Bool) (flush✝ : IO Unit) (read✝ : USize → IO ByteArray) (write✝ : ByteArray → IO Unit) (getLine✝ : IO String) (putStr✝ : String → IO Unit) (isTty✝ : BaseIO Bool) : ({ flush := flush, read := read, write := write, getLine := getLine, putStr := putStr, isTty := isTty } = { flush := flush✝, read := read✝, write := write✝, getLine := getLine✝, putStr := putStr✝, isTty := isTty✝ }) = (flush = flush✝ ∧ read = read✝ ∧ write = write✝ ∧ getLine = getLine✝ ∧ putStr = putStr✝ ∧ isTty = isTty✝)
• Lean.Order.instCCPOIO 📋 Init.Internal.Order.Basic
  {α : Type} : Lean.Order.CCPO (IO α)
• Lean.Order.instMonoBindIO 📋 Init.Internal.Order.Basic
  : Lean.Order.MonoBind IO
• Std.Internal.IO.Async.AsyncTask.block 📋 Std.Internal.Async.Basic
  {α : Type} (x : Std.Internal.IO.Async.AsyncTask α) : IO α
• Std.Internal.IO.Async.Async.ofIOTask 📋 Std.Internal.Async.Basic
  {α : Type} (task : IO (Task α)) : Std.Internal.IO.Async.Async α
• Std.Internal.IO.Async.Async.toIO 📋 Std.Internal.Async.Basic
  {α : Type} (x : Std.Internal.IO.Async.Async α) : IO (Std.Internal.IO.Async.AsyncTask α)
• Std.Internal.IO.Async.Async.block 📋 Std.Internal.Async.Basic
  {α : Type} (x : Std.Internal.IO.Async.Async α) (prio : Task.Priority := Task.Priority.default) : IO α
• Std.Internal.IO.Async.Async.ofPurePromise 📋 Std.Internal.Async.Basic
  {α : Type} (task : IO (IO.Promise α)) (error : String := "the promise linked to the Async was dropped") : Std.Internal.IO.Async.Async α
• Std.Internal.IO.Async.Async.ofPromise 📋 Std.Internal.Async.Basic
  {α : Type} (task : IO (IO.Promise (Except IO.Error α))) (error : String := "the promise linked to the Async was dropped") : Std.Internal.IO.Async.Async α
• Std.Internal.IO.Async.AsyncTask.mapIO 📋 Std.Internal.Async.Basic
  {α β : Type} (f : α → IO β) (x : Std.Internal.IO.Async.AsyncTask α) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : BaseIO (Std.Internal.IO.Async.AsyncTask β)
• Std.Internal.IO.Async.AsyncTask.mapTaskIO 📋 Std.Internal.Async.Basic
  {α β : Type} (f : α → IO β) (x : Std.Internal.IO.Async.AsyncTask α) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : BaseIO (Std.Internal.IO.Async.AsyncTask β)
• Std.Internal.IO.Async.AsyncTask.bindIO 📋 Std.Internal.Async.Basic
  {α β : Type} (x : Std.Internal.IO.Async.AsyncTask α) (f : α → IO (Std.Internal.IO.Async.AsyncTask β)) (prio : Task.Priority := Task.Priority.default) (sync : Bool := false) : BaseIO (Std.Internal.IO.Async.AsyncTask β)
• Std.Internal.IO.Async.Selectable.combine 📋 Std.Internal.Async.Select
  {α : Type} (selectables : Array (Std.Internal.IO.Async.Selectable α)) : IO (Std.Internal.IO.Async.Selector α)
• Std.Internal.Async.IO.AsyncStream.stop 📋 Std.Internal.Async.IO
  {α : Type} {β : outParam Type} [self : Std.Internal.Async.IO.AsyncStream α β] : α → IO Unit
• Std.Internal.Async.IO.AsyncStream.mk 📋 Std.Internal.Async.IO
  {α : Type} {β : outParam Type} (next : α → Std.Internal.IO.Async.Selector β) (stop : α → IO Unit) : Std.Internal.Async.IO.AsyncStream α β
• Std.CloseableChannel.instMonadLiftEIOErrorIO 📋 Std.Sync.Channel
  : MonadLift (EIO Std.CloseableChannel.Error) IO
• Std.Notify.wait 📋 Std.Sync.Notify
  (x : Std.Notify) : IO (Std.Internal.IO.Async.AsyncTask Unit)
• Std.instMonadLiftBroadcastIO 📋 Std.Sync.Broadcast
  : MonadLift (EIO Std.Broadcast.Error) IO
• Std.Broadcast.close 📋 Std.Sync.Broadcast
  {α : Type} (ch : Std.Broadcast α) : IO Unit
• Std.Broadcast.Receiver.unsubscribe 📋 Std.Sync.Broadcast
  {α : Type} (ch : Std.Broadcast.Receiver α) : IO Unit
• Std.Broadcast.subscribe 📋 Std.Sync.Broadcast
  {α : Type} (ch : Std.Broadcast α) : IO (Std.Broadcast.Receiver α)
• Std.Broadcast.Sync.send 📋 Std.Sync.Broadcast
  {α : Type} (ch : Std.Broadcast.Sync α) (v : α) : IO ℕ
• Std.StreamMap.close 📋 Std.Sync.StreamMap
  {α β : Type} (sm : Std.StreamMap α β) : IO Unit
• Std.AnyAsyncStream.getSelector 📋 Std.Sync.StreamMap
  {α : Type} : Std.AnyAsyncStream α → Std.Internal.IO.Async.Selector α × IO Unit
• Std.CancellationToken.wait 📋 Std.Sync.CancellationToken
  (x : Std.CancellationToken) : IO (Std.Internal.IO.Async.AsyncTask Unit)
• Std.Time.Timestamp.now 📋 Std.Time.DateTime.Timestamp
  : IO Std.Time.Timestamp
• Std.Time.Timestamp.since 📋 Std.Time.DateTime.Timestamp
  (f : Std.Time.Timestamp) : IO Std.Time.Duration
• Std.Time.Database.getLocalZoneRules 📋 Std.Time.Zoned.Database.Basic
  {α : Type} [self : Std.Time.Database α] : α → IO Std.Time.TimeZone.ZoneRules
• Std.Time.Database.getZoneRules 📋 Std.Time.Zoned.Database.Basic
  {α : Type} [self : Std.Time.Database α] : α → String → IO Std.Time.TimeZone.ZoneRules
• Std.Time.Database.mk 📋 Std.Time.Zoned.Database.Basic
  {α : Type} (getZoneRules : α → String → IO Std.Time.TimeZone.ZoneRules) (getLocalZoneRules : α → IO Std.Time.TimeZone.ZoneRules) : Std.Time.Database α
• Std.Time.Database.TZdb.localRules 📋 Std.Time.Zoned.Database.TZdb
  (path : System.FilePath) : IO Std.Time.TimeZone.ZoneRules
• Std.Time.Database.TZdb.parseTZIfFromDisk 📋 Std.Time.Zoned.Database.TZdb
  (path : System.FilePath) (id : String) : IO Std.Time.TimeZone.ZoneRules
• Std.Time.Database.TZdb.readRulesFromDisk 📋 Std.Time.Zoned.Database.TZdb
  (path : System.FilePath) (id : String) : IO Std.Time.TimeZone.ZoneRules
• Std.Time.Database.Windows.getLocalTimeZoneIdentifierAt 📋 Std.Time.Zoned.Database.Windows
  : Int64 → IO String
• Std.Time.Database.Windows.getZoneRules 📋 Std.Time.Zoned.Database.Windows
  (id : String) : IO Std.Time.TimeZone.ZoneRules
• Std.Time.Database.Windows.getNextTransition 📋 Std.Time.Zoned.Database.Windows
  : String → Int64 → Bool → IO (Option (Int64 × Std.Time.TimeZone))
• Std.Time.Database.defaultGetLocalZoneRules 📋 Std.Time.Zoned.Database
  : IO Std.Time.TimeZone.ZoneRules
• Std.Time.Database.defaultGetZoneRules 📋 Std.Time.Zoned.Database
  : String → IO Std.Time.TimeZone.ZoneRules
• Std.Time.PlainDate.now 📋 Std.Time.Zoned
  : IO Std.Time.PlainDate
• Std.Time.PlainDateTime.now 📋 Std.Time.Zoned
  : IO Std.Time.PlainDateTime
• Std.Time.PlainTime.now 📋 Std.Time.Zoned
  : IO Std.Time.PlainTime
• Std.Time.ZonedDateTime.now 📋 Std.Time.Zoned
  : IO Std.Time.ZonedDateTime
• Std.Time.ZonedDateTime.nowAt 📋 Std.Time.Zoned
  (id : String) : IO Std.Time.ZonedDateTime
• Std.Time.DateTime.now 📋 Std.Time.Zoned
  {tz : Std.Time.TimeZone} : IO (Std.Time.DateTime tz)
• Std.Time.ZonedDateTime.of 📋 Std.Time.Zoned
  (pdt : Std.Time.PlainDateTime) (id : String) : IO Std.Time.ZonedDateTime
• Std.Tactic.BVDecide.LRAT.loadLRATProof 📋 Std.Tactic.BVDecide.LRAT.Parser
  (path : System.FilePath) : IO (Array Std.Tactic.BVDecide.LRAT.IntAction)
• Std.Tactic.BVDecide.LRAT.dumpLRATProof 📋 Std.Tactic.BVDecide.LRAT.Parser
  (path : System.FilePath) (proof : Array Std.Tactic.BVDecide.LRAT.IntAction) (binaryProofs : Bool) : IO Unit
• Std.Internal.UV.Timer.cancel 📋 Std.Internal.UV.Timer
  (timer : Std.Internal.UV.Timer) : IO Unit
• Std.Internal.UV.Timer.reset 📋 Std.Internal.UV.Timer
  (timer : Std.Internal.UV.Timer) : IO Unit
• Std.Internal.UV.Timer.stop 📋 Std.Internal.UV.Timer
  (timer : Std.Internal.UV.Timer) : IO Unit
• Std.Internal.UV.Timer.mk 📋 Std.Internal.UV.Timer
  (timeout : UInt64) (repeating : Bool) : IO Std.Internal.UV.Timer
• Std.Internal.UV.Timer.next 📋 Std.Internal.UV.Timer
  (timer : Std.Internal.UV.Timer) : IO (IO.Promise Unit)
• Std.Internal.IO.Async.Interval.reset 📋 Std.Internal.Async.Timer
  (i : Std.Internal.IO.Async.Interval) : IO Unit
• Std.Internal.IO.Async.Interval.stop 📋 Std.Internal.Async.Timer
  (i : Std.Internal.IO.Async.Interval) : IO Unit
• Std.Internal.IO.Async.Sleep.stop 📋 Std.Internal.Async.Timer
  (s : Std.Internal.IO.Async.Sleep) : IO Unit
• Std.Internal.IO.Async.Interval.mk 📋 Std.Internal.Async.Timer
  (duration : Std.Time.Millisecond.Offset) : autoParam (0 < duration) Std.Internal.IO.Async.Interval.mk._auto_1 → IO Std.Internal.IO.Async.Interval
• Std.Net.interfaceAddresses 📋 Std.Net.Addr
  : IO (Array Std.Net.InterfaceAddress)
• Std.Internal.UV.TCP.Socket.new 📋 Std.Internal.UV.TCP
  : IO Std.Internal.UV.TCP.Socket
• Std.Internal.UV.TCP.Socket.cancelAccept 📋 Std.Internal.UV.TCP
  (socket : Std.Internal.UV.TCP.Socket) : IO Unit
• Std.Internal.UV.TCP.Socket.cancelRecv 📋 Std.Internal.UV.TCP
  (socket : Std.Internal.UV.TCP.Socket) : IO Unit
• Std.Internal.UV.TCP.Socket.getPeerName 📋 Std.Internal.UV.TCP
  (socket : Std.Internal.UV.TCP.Socket) : IO Std.Net.SocketAddress
• Std.Internal.UV.TCP.Socket.getSockName 📋 Std.Internal.UV.TCP
  (socket : Std.Internal.UV.TCP.Socket) : IO Std.Net.SocketAddress
• Std.Internal.UV.TCP.Socket.noDelay 📋 Std.Internal.UV.TCP
  (socket : Std.Internal.UV.TCP.Socket) : IO Unit
• Std.Internal.UV.TCP.Socket.listen 📋 Std.Internal.UV.TCP
  (socket : Std.Internal.UV.TCP.Socket) (backlog : UInt32) : IO Unit
• Std.Internal.UV.TCP.Socket.bind 📋 Std.Internal.UV.TCP
  (socket : Std.Internal.UV.TCP.Socket) (addr : Std.Net.SocketAddress) : IO Unit
• Std.Internal.UV.TCP.Socket.keepAlive 📋 Std.Internal.UV.TCP
  (socket : Std.Internal.UV.TCP.Socket) (enable : Int8) (delay : UInt32) : IO Unit
• Std.Internal.UV.TCP.Socket.accept 📋 Std.Internal.UV.TCP
  (socket : Std.Internal.UV.TCP.Socket) : IO (IO.Promise (Except IO.Error Std.Internal.UV.TCP.Socket))
• Std.Internal.UV.TCP.Socket.shutdown 📋 Std.Internal.UV.TCP
  (socket : Std.Internal.UV.TCP.Socket) : IO (IO.Promise (Except IO.Error Unit))
• Std.Internal.UV.TCP.Socket.tryAccept 📋 Std.Internal.UV.TCP
  (socket : Std.Internal.UV.TCP.Socket) : IO (Except IO.Error (Option Std.Internal.UV.TCP.Socket))
• Std.Internal.UV.TCP.Socket.waitReadable 📋 Std.Internal.UV.TCP
  (socket : Std.Internal.UV.TCP.Socket) : IO (IO.Promise (Except IO.Error Bool))
• Std.Internal.UV.TCP.Socket.connect 📋 Std.Internal.UV.TCP
  (socket : Std.Internal.UV.TCP.Socket) (addr : Std.Net.SocketAddress) : IO (IO.Promise (Except IO.Error Unit))
• Std.Internal.UV.TCP.Socket.recv? 📋 Std.Internal.UV.TCP
  (socket : Std.Internal.UV.TCP.Socket) (size : UInt64) : IO (IO.Promise (Except IO.Error (Option ByteArray)))
• Std.Internal.UV.TCP.Socket.send 📋 Std.Internal.UV.TCP
  (socket : Std.Internal.UV.TCP.Socket) (data : Array ByteArray) : IO (IO.Promise (Except IO.Error Unit))
• Std.Internal.IO.Async.TCP.Socket.Client.mk 📋 Std.Internal.Async.TCP
  : IO Std.Internal.IO.Async.TCP.Socket.Client
• Std.Internal.IO.Async.TCP.Socket.Server.mk 📋 Std.Internal.Async.TCP
  : IO Std.Internal.IO.Async.TCP.Socket.Server
• Std.Internal.IO.Async.TCP.Socket.Client.getPeerName 📋 Std.Internal.Async.TCP
  (s : Std.Internal.IO.Async.TCP.Socket.Client) : IO Std.Net.SocketAddress
• Std.Internal.IO.Async.TCP.Socket.Client.getSockName 📋 Std.Internal.Async.TCP
  (s : Std.Internal.IO.Async.TCP.Socket.Client) : IO Std.Net.SocketAddress
• Std.Internal.IO.Async.TCP.Socket.Client.noDelay 📋 Std.Internal.Async.TCP
  (s : Std.Internal.IO.Async.TCP.Socket.Client) : IO Unit
• Std.Internal.IO.Async.TCP.Socket.Server.getSockName 📋 Std.Internal.Async.TCP
  (s : Std.Internal.IO.Async.TCP.Socket.Server) : IO Std.Net.SocketAddress
• Std.Internal.IO.Async.TCP.Socket.Server.noDelay 📋 Std.Internal.Async.TCP
  (s : Std.Internal.IO.Async.TCP.Socket.Server) : IO Unit
• Std.Internal.IO.Async.TCP.Socket.Client.bind 📋 Std.Internal.Async.TCP
  (s : Std.Internal.IO.Async.TCP.Socket.Client) (addr : Std.Net.SocketAddress) : IO Unit
• Std.Internal.IO.Async.TCP.Socket.Server.bind 📋 Std.Internal.Async.TCP
  (s : Std.Internal.IO.Async.TCP.Socket.Server) (addr : Std.Net.SocketAddress) : IO Unit
• Std.Internal.IO.Async.TCP.Socket.Server.listen 📋 Std.Internal.Async.TCP
  (s : Std.Internal.IO.Async.TCP.Socket.Server) (backlog : UInt32) : IO Unit
• Std.Internal.IO.Async.TCP.Socket.Server.tryAccept 📋 Std.Internal.Async.TCP
  (s : Std.Internal.IO.Async.TCP.Socket.Server) : IO (Option Std.Internal.IO.Async.TCP.Socket.Client)
• Std.Internal.IO.Async.TCP.Socket.Client.keepAlive 📋 Std.Internal.Async.TCP
  (s : Std.Internal.IO.Async.TCP.Socket.Client) (enable : Bool) (delay : Std.Time.Second.Offset) : autoParam (delay.val ≥ 0) Std.Internal.IO.Async.TCP.Socket.Client.keepAlive._auto_1 → IO Unit
• Std.Internal.IO.Async.TCP.Socket.Server.keepAlive 📋 Std.Internal.Async.TCP
  (s : Std.Internal.IO.Async.TCP.Socket.Server) (enable : Bool) (delay : Std.Time.Second.Offset) : autoParam (delay.val ≥ 1) Std.Internal.IO.Async.TCP.Socket.Server.keepAlive._auto_1 → IO Unit
• Std.Internal.UV.UDP.Socket.new 📋 Std.Internal.UV.UDP
  : IO Std.Internal.UV.UDP.Socket
• Std.Internal.UV.UDP.Socket.cancelRecv 📋 Std.Internal.UV.UDP
  (socket : Std.Internal.UV.UDP.Socket) : IO Unit
• Std.Internal.UV.UDP.Socket.getPeerName 📋 Std.Internal.UV.UDP
  (socket : Std.Internal.UV.UDP.Socket) : IO Std.Net.SocketAddress
• Std.Internal.UV.UDP.Socket.getSockName 📋 Std.Internal.UV.UDP
  (socket : Std.Internal.UV.UDP.Socket) : IO Std.Net.SocketAddress
• Std.Internal.UV.UDP.Socket.setBroadcast 📋 Std.Internal.UV.UDP
  (socket : Std.Internal.UV.UDP.Socket) (on : Bool) : IO Unit
• Std.Internal.UV.UDP.Socket.setMulticastLoop 📋 Std.Internal.UV.UDP
  (socket : Std.Internal.UV.UDP.Socket) (on : Bool) : IO Unit
• Std.Internal.UV.UDP.Socket.setMulticastTTL 📋 Std.Internal.UV.UDP
  (socket : Std.Internal.UV.UDP.Socket) (ttl : UInt32) : IO Unit
• Std.Internal.UV.UDP.Socket.setTTL 📋 Std.Internal.UV.UDP
  (socket : Std.Internal.UV.UDP.Socket) (ttl : UInt32) : IO Unit
• Std.Internal.UV.UDP.Socket.bind 📋 Std.Internal.UV.UDP
  (socket : Std.Internal.UV.UDP.Socket) (addr : Std.Net.SocketAddress) : IO Unit
• Std.Internal.UV.UDP.Socket.connect 📋 Std.Internal.UV.UDP
  (socket : Std.Internal.UV.UDP.Socket) (addr : Std.Net.SocketAddress) : IO Unit
• Std.Internal.UV.UDP.Socket.setMulticastInterface 📋 Std.Internal.UV.UDP
  (socket : Std.Internal.UV.UDP.Socket) (interfaceAddr : Std.Net.IPAddr) : IO Unit
• Std.Internal.UV.UDP.Socket.waitReadable 📋 Std.Internal.UV.UDP
  (socket : Std.Internal.UV.UDP.Socket) : IO (IO.Promise (Except IO.Error Unit))
• Std.Internal.UV.UDP.Socket.setMembership 📋 Std.Internal.UV.UDP
  (socket : Std.Internal.UV.UDP.Socket) (multicastAddr : Std.Net.IPAddr) (interfaceAddr : Option Std.Net.IPAddr) (membership : UInt8) : IO Unit
• Std.Internal.UV.UDP.Socket.recv 📋 Std.Internal.UV.UDP
  (socket : Std.Internal.UV.UDP.Socket) (size : UInt64) : IO (IO.Promise (Except IO.Error (ByteArray × Option Std.Net.SocketAddress)))
• Std.Internal.UV.UDP.Socket.send 📋 Std.Internal.UV.UDP
  (socket : Std.Internal.UV.UDP.Socket) (data : Array ByteArray) (addr : Option Std.Net.SocketAddress) : IO (IO.Promise (Except IO.Error Unit))
• Std.Internal.IO.Async.UDP.Socket.mk 📋 Std.Internal.Async.UDP
  : IO Std.Internal.IO.Async.UDP.Socket
• Std.Internal.IO.Async.UDP.Socket.getPeerName 📋 Std.Internal.Async.UDP
  (s : Std.Internal.IO.Async.UDP.Socket) : IO Std.Net.SocketAddress
• Std.Internal.IO.Async.UDP.Socket.getSockName 📋 Std.Internal.Async.UDP
  (s : Std.Internal.IO.Async.UDP.Socket) : IO Std.Net.SocketAddress
• Std.Internal.IO.Async.UDP.Socket.bind 📋 Std.Internal.Async.UDP
  (s : Std.Internal.IO.Async.UDP.Socket) (addr : Std.Net.SocketAddress) : IO Unit
• Std.Internal.IO.Async.UDP.Socket.connect 📋 Std.Internal.Async.UDP
  (s : Std.Internal.IO.Async.UDP.Socket) (addr : Std.Net.SocketAddress) : IO Unit
• Std.Internal.IO.Async.UDP.Socket.setBroadcast 📋 Std.Internal.Async.UDP
  (s : Std.Internal.IO.Async.UDP.Socket) (enable : Bool) : IO Unit
• Std.Internal.IO.Async.UDP.Socket.setMulticastInterface 📋 Std.Internal.Async.UDP
  (s : Std.Internal.IO.Async.UDP.Socket) (interfaceAddr : Std.Net.IPAddr) : IO Unit
• Std.Internal.IO.Async.UDP.Socket.setMulticastLoop 📋 Std.Internal.Async.UDP
  (s : Std.Internal.IO.Async.UDP.Socket) (enable : Bool) : IO Unit
• Std.Internal.IO.Async.UDP.Socket.setMulticastTTL 📋 Std.Internal.Async.UDP
  (s : Std.Internal.IO.Async.UDP.Socket) (ttl : UInt32) : IO Unit
• Std.Internal.IO.Async.UDP.Socket.setTTL 📋 Std.Internal.Async.UDP
  (s : Std.Internal.IO.Async.UDP.Socket) (ttl : UInt32) : IO Unit
• Std.Internal.IO.Async.UDP.Socket.setMembership 📋 Std.Internal.Async.UDP
  (s : Std.Internal.IO.Async.UDP.Socket) (multicastAddr : Std.Net.IPAddr) (interfaceAddr : Option Std.Net.IPAddr) (membership : Std.Internal.IO.Async.UDP.Membership) : IO Unit
• Std.Internal.UV.System.availableMemory 📋 Std.Internal.UV.System
  : IO UInt64

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 6ff4759 serving mathlib revision c98df61