Loogle!

Result

Found 646 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.Process.output 📋 Init.System.IO
  (args : IO.Process.SpawnArgs) : IO IO.Process.Output
• IO.Process.run 📋 Init.System.IO
  (args : IO.Process.SpawnArgs) : IO String
• 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.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
• 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.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.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.write 📋 Init.System.IO
  (self : IO.FS.Stream) : ByteArray → IO Unit
• IO.FS.Handle.readBinToEndInto.loop 📋 Init.System.IO
  (h : IO.FS.Handle) (acc : ByteArray) : IO ByteArray
• 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.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.FS.lines.read 📋 Init.System.IO
  (h : IO.FS.Handle) (lines : Array String) : IO (Array String)
• 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 α
• 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 β))
• System.FilePath.walkDir.go 📋 Init.System.IO
  (enter : System.FilePath → IO Bool := fun x => pure true) (p : System.FilePath) : StateT (Array System.FilePath) IO Unit
• 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✝)
• Std.Internal.IO.Async.AsyncTask.block 📋 Std.Internal.Async.Basic
  {α : Type} (x : Std.Internal.IO.Async.AsyncTask α) : IO α
• Std.Internal.IO.Async.AsyncTask.mapIO 📋 Std.Internal.Async.Basic
  {α : Type u_1} {β : Type} (f : α → IO β) (x : Std.Internal.IO.Async.AsyncTask α) : BaseIO (Std.Internal.IO.Async.AsyncTask β)
• Std.Internal.IO.Async.AsyncTask.bindIO 📋 Std.Internal.Async.Basic
  {α : Type u_1} {β : Type} (x : Std.Internal.IO.Async.AsyncTask α) (f : α → IO (Std.Internal.IO.Async.AsyncTask β)) : BaseIO (Std.Internal.IO.Async.AsyncTask β)
• Std.Internal.IO.Async.Selector.unregisterFn 📋 Std.Internal.Async.Select
  {α : Type} (self : Std.Internal.IO.Async.Selector α) : IO Unit
• Std.Internal.IO.Async.Selector.tryFn 📋 Std.Internal.Async.Select
  {α : Type} (self : Std.Internal.IO.Async.Selector α) : IO (Option α)
• Std.Internal.IO.Async.Selectable.one 📋 Std.Internal.Async.Select
  {α : Type} (selectables : Array (Std.Internal.IO.Async.Selectable α)) : IO (Std.Internal.IO.Async.AsyncTask α)
• Std.Internal.IO.Async.Selector.registerFn 📋 Std.Internal.Async.Select
  {α : Type} (self : Std.Internal.IO.Async.Selector α) : Std.Internal.IO.Async.Waiter α → IO Unit
• Std.Internal.IO.Async.Selectable.cont 📋 Std.Internal.Async.Select
  {α : Type} (self : Std.Internal.IO.Async.Selectable α) : self.β → IO (Std.Internal.IO.Async.AsyncTask α)
• Std.Internal.IO.Async.Selectable.case 📋 Std.Internal.Async.Select
  {α β : Type} (selector : Std.Internal.IO.Async.Selector β) (cont : β → IO (Std.Internal.IO.Async.AsyncTask α)) : Std.Internal.IO.Async.Selectable α
• Std.Internal.IO.Async.Selector.mk 📋 Std.Internal.Async.Select
  {α : Type} (tryFn : IO (Option α)) (registerFn : Std.Internal.IO.Async.Waiter α → IO Unit) (unregisterFn : IO Unit) : Std.Internal.IO.Async.Selector α
• Std.Internal.IO.Async.Selector.mk.sizeOf_spec 📋 Std.Internal.Async.Select
  {α : Type} [SizeOf α] (tryFn : IO (Option α)) (registerFn : Std.Internal.IO.Async.Waiter α → IO Unit) (unregisterFn : IO Unit) : sizeOf { tryFn := tryFn, registerFn := registerFn, unregisterFn := unregisterFn } = 1
• Std.Internal.IO.Async.Selectable.case.injEq 📋 Std.Internal.Async.Select
  {α β : Type} (selector : Std.Internal.IO.Async.Selector β) (cont : β → IO (Std.Internal.IO.Async.AsyncTask α)) (β✝ : Type) (selector✝ : Std.Internal.IO.Async.Selector β✝) (cont✝ : β✝ → IO (Std.Internal.IO.Async.AsyncTask α)) : ({ β := β, selector := selector, cont := cont } = { β := β✝, selector := selector✝, cont := cont✝ }) = (β = β✝ ∧ HEq selector selector✝ ∧ HEq cont cont✝)
• Std.Internal.IO.Async.Selector.mk.injEq 📋 Std.Internal.Async.Select
  {α : Type} (tryFn : IO (Option α)) (registerFn : Std.Internal.IO.Async.Waiter α → IO Unit) (unregisterFn : IO Unit) (tryFn✝ : IO (Option α)) (registerFn✝ : Std.Internal.IO.Async.Waiter α → IO Unit) (unregisterFn✝ : IO Unit) : ({ tryFn := tryFn, registerFn := registerFn, unregisterFn := unregisterFn } = { tryFn := tryFn✝, registerFn := registerFn✝, unregisterFn := unregisterFn✝ }) = (tryFn = tryFn✝ ∧ registerFn = registerFn✝ ∧ unregisterFn = unregisterFn✝)
• Std.Internal.IO.Async.Selectable.case.sizeOf_spec 📋 Std.Internal.Async.Select
  {α : Type} [SizeOf α] {β : Type} (selector : Std.Internal.IO.Async.Selector β) (cont : β → IO (Std.Internal.IO.Async.AsyncTask α)) : sizeOf { β := β, selector := selector, cont := cont } = 1 + sizeOf β + sizeOf selector
• Std.CloseableChannel.instMonadLiftEIOErrorIO 📋 Std.Sync.Channel
  : MonadLift (EIO Std.CloseableChannel.Error) IO
• 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.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.mk 📋 Std.Internal.Async.Timer
  (duration : Std.Time.Millisecond.Offset) : IO Std.Internal.IO.Async.Sleep
• Std.Internal.IO.Async.Sleep.reset 📋 Std.Internal.Async.Timer
  (s : Std.Internal.IO.Async.Sleep) : IO Unit
• Std.Internal.IO.Async.Sleep.stop 📋 Std.Internal.Async.Timer
  (s : Std.Internal.IO.Async.Sleep) : IO Unit
• Std.Internal.IO.Async.sleep 📋 Std.Internal.Async.Timer
  (duration : Std.Time.Millisecond.Offset) : IO (Std.Internal.IO.Async.AsyncTask Unit)
• Std.Internal.IO.Async.Interval.tick 📋 Std.Internal.Async.Timer
  (i : Std.Internal.IO.Async.Interval) : IO (Std.Internal.IO.Async.AsyncTask Unit)
• Std.Internal.IO.Async.Selector.sleep 📋 Std.Internal.Async.Timer
  (duration : Std.Time.Millisecond.Offset) : IO (Std.Internal.IO.Async.Selector Unit)
• Std.Internal.IO.Async.Sleep.selector 📋 Std.Internal.Async.Timer
  (s : Std.Internal.IO.Async.Sleep) : IO (Std.Internal.IO.Async.Selector Unit)
• Std.Internal.IO.Async.Sleep.wait 📋 Std.Internal.Async.Timer
  (s : Std.Internal.IO.Async.Sleep) : IO (Std.Internal.IO.Async.AsyncTask Unit)
• Std.Internal.IO.Async.Interval.mk 📋 Std.Internal.Async.Timer
  (duration : Std.Time.Millisecond.Offset) : autoParam (0 < duration) _auto✝ → 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.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.waitReadable 📋 Std.Internal.UV.TCP
  (socket : Std.Internal.UV.TCP.Socket) : IO (IO.Promise (Except IO.Error Bool))
• Std.Internal.UV.TCP.Socket.send 📋 Std.Internal.UV.TCP
  (socket : Std.Internal.UV.TCP.Socket) (data : ByteArray) : IO (IO.Promise (Except IO.Error Unit))
• 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.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.Client.shutdown 📋 Std.Internal.Async.TCP
  (s : Std.Internal.IO.Async.TCP.Socket.Client) : IO (Std.Internal.IO.Async.AsyncTask Unit)
• Std.Internal.IO.Async.TCP.Socket.Server.accept 📋 Std.Internal.Async.TCP
  (s : Std.Internal.IO.Async.TCP.Socket.Server) : IO (Std.Internal.IO.Async.AsyncTask Std.Internal.IO.Async.TCP.Socket.Client)
• 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.Client.connect 📋 Std.Internal.Async.TCP
  (s : Std.Internal.IO.Async.TCP.Socket.Client) (addr : Std.Net.SocketAddress) : IO (Std.Internal.IO.Async.AsyncTask Unit)
• Std.Internal.IO.Async.TCP.Socket.Client.send 📋 Std.Internal.Async.TCP
  (s : Std.Internal.IO.Async.TCP.Socket.Client) (data : ByteArray) : IO (Std.Internal.IO.Async.AsyncTask Unit)
• Std.Internal.IO.Async.TCP.Socket.Client.recv? 📋 Std.Internal.Async.TCP
  (s : Std.Internal.IO.Async.TCP.Socket.Client) (size : UInt64) : IO (Std.Internal.IO.Async.AsyncTask (Option ByteArray))
• Std.Internal.IO.Async.TCP.Socket.Client.recvSelector 📋 Std.Internal.Async.TCP
  (s : Std.Internal.IO.Async.TCP.Socket.Client) (size : UInt64) : IO (Std.Internal.IO.Async.Selector (Option ByteArray))
• 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) _auto✝ → 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) _auto✝ → 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.send 📋 Std.Internal.UV.UDP
  (socket : Std.Internal.UV.UDP.Socket) (data : ByteArray) (addr : Option Std.Net.SocketAddress) : IO (IO.Promise (Except IO.Error 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.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.IO.Async.UDP.Socket.recv 📋 Std.Internal.Async.UDP
  (s : Std.Internal.IO.Async.UDP.Socket) (size : UInt64) : IO (Std.Internal.IO.Async.AsyncTask (ByteArray × Option Std.Net.SocketAddress))
• Std.Internal.IO.Async.UDP.Socket.recvSelector 📋 Std.Internal.Async.UDP
  (s : Std.Internal.IO.Async.UDP.Socket) (size : UInt64) : IO (Std.Internal.IO.Async.Selector (ByteArray × Option Std.Net.SocketAddress))
• Std.Internal.IO.Async.UDP.Socket.send 📋 Std.Internal.Async.UDP
  (s : Std.Internal.IO.Async.UDP.Socket) (data : ByteArray) (addr : Option Std.Net.SocketAddress := none) : IO (Std.Internal.IO.Async.AsyncTask Unit)
• Lean.enableInitializersExecution 📋 Lean.ImportingFlag
  : IO Unit
• Lean.initializing 📋 Lean.ImportingFlag
  : IO Bool
• Lean.isInitializerExecutionEnabled 📋 Lean.ImportingFlag
  : IO Bool

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 19971e9 serving mathlib revision 44f2e31