Mutable data types

Stream: new members

[Arjun Viswanathan]

Does lean have mutable datatypes?

[Yakov Pechersky]

Would d_array count as one?

[Eric Wieser]

docs#d_array

[Arjun Viswanathan]

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?

[Eric Wieser]

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

[Eric Wieser]

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

[Mario Carneiro]

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

[Mario Carneiro]

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