IO options when using lake

Stream: general

[Riley Beckett]

Hi. Nice to meet you all.

I've set up a lake build so that entering ./build/bin/datatypes > output.txt in terminal writes to the text file output.txt.

Meanwhile the corresponding main file produces this:

def main : IO Unit :=
IO.println "Example"

My next goal is to find a function which converts any lean object named X1...Xn to the string "X1...Xn". Really I want a print function which is far more general, and simply prints the name of the object contained in the result.

What sorts of options are there besides IO.println (which takes a string)?

[Henrik Böving]

Lean objects dont inherently have a name, you might want to take a look into docs4#ToString which provides a general API for printing out the value of a lean object