Skip to content

Type of main #138

Open
Open
@LeventErkok

Description

@LeventErkok

This section suggests main can only have 3 different types:

An `IO` action `main` is executed when the program starts.
`main` can have one of three types:
* `main : IO Unit` is used for simple programs that cannot read their command-line arguments and always return exit code `0`,
* `main : IO UInt32` is used for programs without arguments that may signal success or failure, and
* `main : List String → IO UInt32` is used for programs that take command-line arguments and signal success or failure.

I think main : List String → IO Unit is a 4th alternative, which lean seems to accept just fine.

Not a terribly important point, but I was confused as to why that wouldn't be allowed. Would be good to clarify.

Metadata

Metadata

Assignees

No one assigned

    Labels

    TypoTypographical or grammatical errors in the text

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions