Zulip Chat Archive

Stream: lean4

Topic: How to run `main`?

view this post on Zulip Wojciech Nawrocki (Jan 06 2021 at 21:49):

The List String is a list of command line arguments, which in the editor you could just simulate with #eval main [] (or a non-empty list if the program actually needs some arguments).

Last updated: May 18 2021 at 23:14 UTC