Stream: new members
Topic: Mutable data types
Arjun Viswanathan (Feb 19 2021 at 15:53):
Does lean have mutable datatypes?
Yakov Pechersky (Feb 19 2021 at 15:54):
d_array count as one?
Eric Wieser (Feb 19 2021 at 15:55):
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?
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
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
Mario Carneiro (Feb 20 2021 at 00:52):
There is a
ref type, that you can use in tactics
Mario Carneiro (Feb 20 2021 at 00:53):
The more FP way to do this is to use a
Last updated: May 08 2021 at 09:11 UTC