Idris2Doc : Idrall.Path

Idrall.Path

(source)

Definitions

Dir : Type
Visibility: public export
dataPath : Type
Totality: total
Visibility: public export
Constructors:
Home : Dir->Path
Absolute : Dir->Path
Relative : Dir->Path

Hint: 
ShowPath
recordFilePath : Type
Totality: total
Visibility: public export
Constructor: 
MkFilePath : Path->MaybeString->FilePath

Projections:
.fileName : FilePath->MaybeString
.path : FilePath->Path

Hints:
EqFilePath
PrettyFilePath
ShowFilePath
.path : FilePath->Path
Visibility: public export
path : FilePath->Path
Visibility: public export
.fileName : FilePath->MaybeString
Visibility: public export
fileName : FilePath->MaybeString
Visibility: public export
normalisePath : Dir->Dir
Visibility: public export
normaliseFilePath : FilePath->FilePath
Visibility: public export
pathFromDir : Dir->Path
Visibility: public export
addSlashes : Dir->String
Visibility: public export
prettyPrintPath : Path->String
Visibility: public export
splitOnFile : Dir-> (Dir, MaybeString)
Visibility: public export
mkFilePath : (Dir, MaybeString) -> (Dir->Path) ->FilePath
Visibility: public export
filePathFromPath : Path->FilePath
Visibility: public export
filePathForIO : FilePath->String
Visibility: public export