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
record Timestamp : Type
  Record that holds timestamps with nanosecond precision

Totality: total
Visibility: public export
Constructor: 
MkTimestamp : Int -> Int -> Timestamp

Projections:
.nsec : Timestamp -> Int
.sec : Timestamp -> Int

Hints:
Eq Timestamp
Ord Timestamp
Show Timestamp
.sec : Timestamp -> Int
Totality: total
Visibility: public export
sec : Timestamp -> Int
Totality: total
Visibility: public export
.nsec : Timestamp -> Int
Totality: total
Visibility: public export
nsec : Timestamp -> Int
Totality: total
Visibility: public export
record FileTime : Type
  Record that holds file's time attributes

Totality: total
Visibility: public export
Constructor: 
MkFileTime : Timestamp -> Timestamp -> Timestamp -> FileTime

Projections:
.atime : FileTime -> Timestamp
.ctime : FileTime -> Timestamp
.mtime : FileTime -> Timestamp
.atime : FileTime -> Timestamp
Totality: total
Visibility: public export
atime : FileTime -> Timestamp
Totality: total
Visibility: public export
.mtime : FileTime -> Timestamp
Totality: total
Visibility: public export
mtime : FileTime -> Timestamp
Totality: total
Visibility: public export
.ctime : FileTime -> Timestamp
Totality: total
Visibility: public export
ctime : FileTime -> Timestamp
Totality: total
Visibility: public export
fileTime : HasIO io => File -> io (Either FileError FileTime)
  Get File's time attributes

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