Zulip Chat Archive

Stream: general

Topic: nat to string?


view this post on Zulip Scott Morrison (Apr 09 2018 at 23:49):

How to I get a string from a nat?

view this post on Zulip Simon Hudon (Apr 09 2018 at 23:52):

to_string

view this post on Zulip Scott Morrison (Apr 09 2018 at 23:53):

invalid field notation, 'to_string' is not a valid "field" because environment does not contain 'nat.to_string'
  k
which has type
  ℕ

view this post on Zulip Simon Hudon (Apr 09 2018 at 23:55):

try to_string k. It's part of the has_to_string class so it won't support field notation

view this post on Zulip Scott Morrison (Apr 09 2018 at 23:55):

thank you!


Last updated: May 12 2021 at 05:19 UTC