Compiler settings

We use lean 4.29.1 to compile your program with the following command:

$ lean {mainfile}

• {mainfile} is the entrypoint file (you can specify which file this is when submitting).

Runtime settings

We use lean 4.29.1 to run your program with the following command:

$ lean --run {mainfile}

• {mainfile} is the entrypoint file (you can specify which file this is when submitting).

File extensions

Files with any of the following file extensions will be used: .lean

Additional information

Additional language-specific advice and information for many languages is available in the knowledge base