Idris2Doc : System.Console.GetOpt

System.Console.GetOpt

This library provides facilities for parsing the command-line options
in a standalone program. It is essentially an Idris port of the GNU getopt library.
(Actually, it is an Idris port of the [corresponding Haskell module]
(http://hackage.haskell.org/package/base-4.14.1.0/docs/System-Console-GetOpt.html)).

Definitions

dataArgOrder : Type->Type
  What to do with options following non-options

Totality: total
Visibility: public export
Constructors:
RequireOrder : ArgOrdera
  no option processing after first non-option
Permute : ArgOrdera
  freely intersperse options and non-options
ReturnInOrder : (String->a) ->ArgOrdera
  wrap non-options into options

Hint: 
FunctorArgOrder
dataArgDescr : Type->Type
  Describes whether an option takes an argument or not, and if so
how the argument is injected into a value of type `a`.

Totality: total
Visibility: public export
Constructors:
NoArg : a->ArgDescra
  no argument expected
ReqArg : (String->a) ->String->ArgDescra
  option requires argument
OptArg : (MaybeString->a) ->String->ArgDescra
  optional argument

Hint: 
FunctorArgDescr
recordOptDescr : Type->Type
  Each `OptDescr` describes a single option.

The arguments to 'Option' are:

* list of short option characters
* list of long option strings (without \"--\")
* argument descriptor
* explanation of option for user

Totality: total
Visibility: public export
Constructor: 
MkOpt : ListChar->ListString->ArgDescra->String->OptDescra

Projections:
.argDescr : OptDescra->ArgDescra
  argument descriptor
.description : OptDescra->String
  explanation of option for user
.longNames : OptDescra->ListString
  list of long option strings (without "--")
.shortNames : OptDescra->ListChar
  list of short option characters

Hint: 
FunctorOptDescr
.shortNames : OptDescra->ListChar
  list of short option characters

Totality: total
Visibility: public export
shortNames : OptDescra->ListChar
  list of short option characters

Totality: total
Visibility: public export
.longNames : OptDescra->ListString
  list of long option strings (without "--")

Totality: total
Visibility: public export
longNames : OptDescra->ListString
  list of long option strings (without "--")

Totality: total
Visibility: public export
.argDescr : OptDescra->ArgDescra
  argument descriptor

Totality: total
Visibility: public export
argDescr : OptDescra->ArgDescra
  argument descriptor

Totality: total
Visibility: public export
.description : OptDescra->String
  explanation of option for user

Totality: total
Visibility: public export
description : OptDescra->String
  explanation of option for user

Totality: total
Visibility: public export
usageInfo : String->List (OptDescra) ->String
  Return a string describing the usage of a command, derived from
the header (first argument) and the options described by the
second argument.

Totality: total
Visibility: public export
recordResult : Type->Type
  Result of parsing the command line arguments accoring to a list
of `OptDescr`s. (see also function `getOpt`).

Totality: total
Visibility: public export
Constructor: 
MkResult : Lista->ListString->ListString->ListString->Resulta

Projections:
.errors : Resulta->ListString
  Errors during option parsing. These occur, for instance, when
an option requires an additional argument but none was given.
.nonOptions : Resulta->ListString
  List of non-options (other command line arguments)
.options : Resulta->Lista
  List of successfully parsed options
.unrecognized : Resulta->ListString
  List of unrecognized options.

Hint: 
FunctorResult
.options : Resulta->Lista
  List of successfully parsed options

Totality: total
Visibility: public export
options : Resulta->Lista
  List of successfully parsed options

Totality: total
Visibility: public export
.nonOptions : Resulta->ListString
  List of non-options (other command line arguments)

Totality: total
Visibility: public export
nonOptions : Resulta->ListString
  List of non-options (other command line arguments)

Totality: total
Visibility: public export
.unrecognized : Resulta->ListString
  List of unrecognized options.

Totality: total
Visibility: public export
unrecognized : Resulta->ListString
  List of unrecognized options.

Totality: total
Visibility: public export
.errors : Resulta->ListString
  Errors during option parsing. These occur, for instance, when
an option requires an additional argument but none was given.

Totality: total
Visibility: public export
errors : Resulta->ListString
  Errors during option parsing. These occur, for instance, when
an option requires an additional argument but none was given.

Totality: total
Visibility: public export
emptyRes : Resulta
Totality: total
Visibility: public export
getOpt : ArgOrdera->List (OptDescra) ->ListString->Resulta
  Process the command-line, and return the list of values that matched
(and those that didn't). The arguments are:

* The order requirements (see `ArgOrder`)

* The option descriptions (see `OptDescr`)

* The actual command line arguments (presumably got from
`System.getArgs`).

Totality: total
Visibility: export