IO and Char utilities from the library

Stream: lean4

[Phil Nguyen]

Hi, I'm attempting to participate in these benchmarks to see how Lean performs. I've written most of the BF interpreter, but need help with the following primitives to complete the benchmark:

• IO functions for flushing the output stream
• Function for reading an environment variable
• Function for reading commandline arguments
• Function for incrementing/decrementing Char (or converting Char to and from fixed width integer, or at least Nat)

I've looked in the source code in lean4/src/Init/System/ but haven't found those. Another question is can I browse the library documentation somewhere, or github is the only place for now?

Many thanks!!

[Mario Carneiro]

• IO functions for flushing the output stream: FS.Stream.flush
• Function for reading an environment variable: IO.getEnv
• Function for reading commandline arguments: def main (args : List String) : IO UInt32 := ...
• Function for incrementing/decrementing Char (or converting Char to and from fixed width integer, or at least Nat): Char.toNat, Char.val

[Mario Carneiro]

You probably want to use UInt8 instead of Char though; Char has a messy domain since it's a unicode scalar value