Zulip Chat Archive

Stream: new members

Topic: printing formatted strings


view this post on Zulip Kris Brown (Jul 02 2020 at 23:57):

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?

view this post on Zulip Mario Carneiro (Jul 03 2020 at 00:34):

#mwe?

view this post on Zulip Mario Carneiro (Jul 03 2020 at 00:36):

#eval tactic.trace "hello world"

view this post on Zulip Mario Carneiro (Jul 03 2020 at 00:36):

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

view this post on Zulip Kris Brown (Jul 03 2020 at 00:37):

Thanks, io.put_str works perfectly!

view this post on Zulip Mario Carneiro (Jul 03 2020 at 00:38):

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

Last updated: May 16 2021 at 05:21 UTC