Idris2Doc : Options

Options

(source)

Definitions

recordConfig : Type
  Program Config

Totality: total
Visibility: public export
Constructor: 
MkConfig : Bool->Nat->Bool->Bool->Bool->ListBody->ListFilePath->Config

Projections:
.checkOnly : Config->Bool
  True, if files should only be checked for issues
without fixing their content.
.extensions : Config->ListBody
  List of file extensions to be checked when traversing
directories. If `includeAll` is set to `True`, this
is ignored.
.files : Config->ListFilePath
  List of files and directories to be checked.
.includeAll : Config->Bool
  True, if all non-hidden files should be checked when
traversing directories.
.includeHidden : Config->Bool
  True, if hidden files should be checked when
traversing directories.
.printHelp : Config->Bool
  If True, prints only the program synopsis.
.verbosity : Config->Nat
  Verbosity level. At the moment, 0 means total silence (errors are
still printed to stderr) while 4 is most talkative.

Hints:
EqConfig
PrettyConfig
ShowConfig
.printHelp : Config->Bool
  If True, prints only the program synopsis.

Totality: total
Visibility: public export
printHelp : Config->Bool
  If True, prints only the program synopsis.

Totality: total
Visibility: public export
.verbosity : Config->Nat
  Verbosity level. At the moment, 0 means total silence (errors are
still printed to stderr) while 4 is most talkative.

Totality: total
Visibility: public export
verbosity : Config->Nat
  Verbosity level. At the moment, 0 means total silence (errors are
still printed to stderr) while 4 is most talkative.

Totality: total
Visibility: public export
.checkOnly : Config->Bool
  True, if files should only be checked for issues
without fixing their content.

Totality: total
Visibility: public export
checkOnly : Config->Bool
  True, if files should only be checked for issues
without fixing their content.

Totality: total
Visibility: public export
.includeAll : Config->Bool
  True, if all non-hidden files should be checked when
traversing directories.

Totality: total
Visibility: public export
includeAll : Config->Bool
  True, if all non-hidden files should be checked when
traversing directories.

Totality: total
Visibility: public export
.includeHidden : Config->Bool
  True, if hidden files should be checked when
traversing directories.

Totality: total
Visibility: public export
includeHidden : Config->Bool
  True, if hidden files should be checked when
traversing directories.

Totality: total
Visibility: public export
.extensions : Config->ListBody
  List of file extensions to be checked when traversing
directories. If `includeAll` is set to `True`, this
is ignored.

Totality: total
Visibility: public export
extensions : Config->ListBody
  List of file extensions to be checked when traversing
directories. If `includeAll` is set to `True`, this
is ignored.

Totality: total
Visibility: public export
.files : Config->ListFilePath
  List of files and directories to be checked.

Totality: total
Visibility: public export
files : Config->ListFilePath
  List of files and directories to be checked.

Totality: total
Visibility: public export
includeDir : FilePath->Config->Bool
  Tests, whether a file or directory is hidden and should
still be included.

Totality: total
Visibility: export
includeFile : FilePath->Config->Bool
  Tests, whether a file should be included when traversing
a directory.

Totality: total
Visibility: export
applyArgs : ListString->Either (ListString) Config
Totality: total
Visibility: export
info : String
Totality: total
Visibility: export
shortInfo : String
Totality: total
Visibility: export