mkdir : String -> Mode -> EPrim () Creates a new directory.
This fails if the directory exists already. It also fails, if the
parent directory does not exist.
Totality: total
Visibility: exportopendir : String -> EPrim Dir Opens a directory.
Totality: total
Visibility: exportfdopendir : FileDesc a => a -> EPrim Dir Opens a directory from a file descriptor.
Totality: total
Visibility: exportrewinddir : Dir -> PrimIO () Rewinds a directory.
Totality: total
Visibility: exportclosedir : Dir -> EPrim () Closes a directory.
Totality: total
Visibility: exportclosedir' : Dir -> F1' World Closes a directory.
Totality: total
Visibility: exportreaddir : (0 r : Type) -> FromBuf r => Dir -> EPrim (ReadRes r) Reads the next entry from a directory.
Totality: total
Visibility: exportgetcwd : (0 r : Type) -> FromBuf r => EPrim r Returns the current working directory.
Totality: total
Visibility: exportchdir : String -> EPrim () Changes the current working directory
Totality: total
Visibility: exportchroot : String -> EPrim () Changes the current working directory
Totality: total
Visibility: export