printing formatted strings

Stream: new members

[Kris Brown]

I often write string methods for data structures and #eval the results of function applications to see if I implemented them correctly. When I do this, \n newlines aren't formatted in the Lean Goal panel in VS code. Is there a way to view formatted strings?

[Mario Carneiro]

#mwe?

[Mario Carneiro]

#eval tactic.trace "hello world"

[Mario Carneiro]

import system.io
#eval io.put_str "hello world"

[Kris Brown]

Thanks, io.put_str works perfectly!

[Mario Carneiro]

structure foo := (s : string)
instance : has_repr foo := ⟨foo.s⟩
#eval foo.mk "hello world"