Zulip Chat Archive

Stream: new members

Topic: Mutable data types


view this post on Zulip Arjun Viswanathan (Feb 19 2021 at 15:53):

Does lean have mutable datatypes?

view this post on Zulip Yakov Pechersky (Feb 19 2021 at 15:54):

Would d_array count as one?

view this post on Zulip Eric Wieser (Feb 19 2021 at 15:55):

docs#d_array

view this post on Zulip Arjun Viswanathan (Feb 19 2021 at 15:57):

I suppose persistent arrays do count. I'm trying to create a global natural number counter, is there a ref type that I can use with nats?

view this post on Zulip Eric Wieser (Feb 19 2021 at 15:59):

As far as I can tell,d_array isn't "mutable" in the normal sense of the word, it just has the performance implications of a mutable array

view this post on Zulip Eric Wieser (Feb 19 2021 at 16:00):

You're supposed to use the return value of d_array.write which contains the modified array, I believe

view this post on Zulip Mario Carneiro (Feb 20 2021 at 00:52):

There is a ref type, that you can use in tactics

view this post on Zulip Mario Carneiro (Feb 20 2021 at 00:53):

The more FP way to do this is to use a state monad


Last updated: May 08 2021 at 09:11 UTC