A variant of #eval for 2D ASCII art?

Stream: new members

[Eduardo Ochs]

Hi all, I've just adapted this thing -

http://anggtwu.net/eev-maxima.html#luatree

to Lean4, but I'm not being able to find an alternative to #eval that would display my 2D trees in ASCII art bidimensionally... #eval is displaying the line breaks as "\n"s, as shown in the screenshot below. Help needed! Suggestions, please?

sshot.png

[Damiano Testa]

Does #eval do IO.println (← yourIOstring) work?

[Eduardo Ochs]

Brilliant! Thanks! =)

[Mario Carneiro]

Also, the output there is produced by the Repr instance for the return value's type, so if you implement it to produce a string directly instead of using the Repr String instance (which escapes the characters) it will be drawn as you intend