structure Network.Sendfile.FilePart : Type

A portion of a file to send.

• offset : Nat

  Offset in bytes from start of file.

• count : Nat

  Number of bytes to send. 0 means to end of file.

def Network.Sendfile.instBEqFilePart.beq : FilePart → FilePart → Bool

Equations

• Network.Sendfile.instBEqFilePart.beq { offset := a, count := a_1 } { offset := b, count := b_1 } = (a == b && a_1 == b_1)
• Network.Sendfile.instBEqFilePart.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Network.Sendfile.instBEqFilePart : BEq FilePart

Equations

• Network.Sendfile.instBEqFilePart = { beq := Network.Sendfile.instBEqFilePart.beq }

def Network.Sendfile.instReprFilePart.repr : FilePart → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Network.Sendfile.instReprFilePart : Repr FilePart

Equations

• Network.Sendfile.instReprFilePart = { reprPrec := Network.Sendfile.instReprFilePart.repr }

def Network.Sendfile.sendFile (sock : Socket.Socket Socket.SocketState.connected) (path : String) (part : Option FilePart := none) : IO Unit

Send a file (or portion thereof) over a connected socket. Uses read+send fallback implementation. $$\text{sendFile} : \text{Socket}\ \texttt{.connected} \to \text{String} \to \text{Option}(\text{FilePart}) \to \text{IO}(\text{Unit})$$

Equations

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

@[inline]

def Network.Sendfile.sendFileSimple (sock : Socket.Socket Socket.SocketState.connected) (path : String) : IO Unit

Send an entire file over a connected socket. $$\text{sendFileSimple} : \text{Socket}\ \texttt{.connected} \to \text{String} \to \text{IO}(\text{Unit})$$

Equations

• Network.Sendfile.sendFileSimple sock path = Network.Sendfile.sendFile sock path