Idris2Doc : System.File.Meta

System.File.Meta

Functions for accessing file metadata.

Reexports

import public System.File.Types

Definitions

exists : HasIO io => String -> io Bool
  Check if a file exists for reading.

Totality: total
Visibility: export
firstExists : HasIO io => List String -> io (Maybe String)
  Pick the first existing file

Totality: total
Visibility: export
fileAccessTime : HasIO io => File -> io (Either FileError Int)
  Get the File's atime.

Totality: total
Visibility: export
fileModifiedTime : HasIO io => File -> io (Either FileError Int)
  Get the File's mtime.

Totality: total
Visibility: export
fileStatusTime : HasIO io => File -> io (Either FileError Int)
  Get the File's ctime.

Totality: total
Visibility: export
fileSize : HasIO io => File -> io (Either FileError Int)
  Get the File's size.

Totality: total
Visibility: export
fPoll : HasIO io => File -> io Bool
  Check whether the given File's size is non-zero.

Totality: total
Visibility: export
isTTY : HasIO io => File -> io Bool
  Check whether the given File is a terminal device.

Totality: total
Visibility: export