structure System.Posix.Fd : Type

A file descriptor (Unix fd number).

• fd : UInt32

def System.Posix.instBEqFd.beq : Fd → Fd → Bool

Equations

• System.Posix.instBEqFd.beq { fd := a } { fd := b } = (a == b)
• System.Posix.instBEqFd.beq x✝¹ x✝ = false

@[implicit_reducible]

instance System.Posix.instBEqFd : BEq Fd

Equations

• System.Posix.instBEqFd = { beq := System.Posix.instBEqFd.beq }

@[implicit_reducible]

instance System.Posix.instReprFd : Repr Fd

Equations

• System.Posix.instReprFd = { reprPrec := System.Posix.instReprFd.repr }

def System.Posix.instReprFd.repr : Fd → Nat → Std.Format

Equations

• System.Posix.instReprFd.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "fd" ++ Std.Format.text " := " ++ (Std.Format.nest 6 (repr x✝.fd)).group) " }"

@[implicit_reducible]

instance System.Posix.instInhabitedFd : Inhabited Fd

Equations

• System.Posix.instInhabitedFd = { default := System.Posix.instInhabitedFd.default }

def System.Posix.instInhabitedFd.default : Fd

Equations

• System.Posix.instInhabitedFd.default = { fd := default }

@[implicit_reducible]

instance System.Posix.instToStringFd : ToString Fd

Equations

• System.Posix.instToStringFd = { toString := fun (f : System.Posix.Fd) => toString "Fd(" ++ toString f.fd ++ toString ")" }

def System.Posix.closeFd : Fd → IO Unit

Close a file descriptor.

Equations

• System.Posix.closeFd x✝ = pure ()

structure System.Posix.FileStatus : Type

File status information (simplified).

• size : Nat
• isRegularFile : Bool
• isDirectory : Bool

@[implicit_reducible]

instance System.Posix.instReprFileStatus : Repr FileStatus

Equations

• System.Posix.instReprFileStatus = { reprPrec := System.Posix.instReprFileStatus.repr }

def System.Posix.instReprFileStatus.repr : FileStatus → Nat → Std.Format

Equations

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

def System.Posix.getFileStatus (path : String) : IO FileStatus

Get file status. $$\text{getFileStatus} : \text{String} \to \text{IO}(\text{FileStatus})$$

Equations

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

def System.Posix.fileExist (path : String) : IO Bool

Check if a file exists.

Equations

• System.Posix.fileExist path = tryCatch (do let __discr ← { toString := path }.metadata have x : IO.FS.Metadata := __discr pure true) fun (x : IO.Error) => pure false