cli args

Stream: new members

[crab]

can you take in command line arguments in lean?

[Adam Topaz]

In lean 4, you can do, e.g., the following:

def main (L : List String) : IO Unit :=
for l in L do
  IO.println l

and the command line arguments will be passed in as the list of strings to the main function. I don't know how to do this in lean3.

[Adam Topaz]

In fact, I realized now I don't even know how to compile lean3 code into a binary...

[Julian Berman]

io.cmdline_args it looks like

[Julian Berman]

e.g. https://github.com/leanprover-community/lean/blob/65ad4ffdb3abac75be748554e3cbe990fb1c6500/tests/lean/run/socket_client.lean#L16-L21 (which I just found by github serach)

[crab]

Adam Topaz said:

In lean 4, you can do, e.g., the following:

def main (L : List String) : IO Unit :=
for l in L do
  IO.println l

and the command line arguments will be passed in as the list of strings to the main function. I don't know how to do this in lean3.

thank you