LeanMPZ and LeanStructArray runtime objects

Stream: lean4

[Yuri]

These two object tags are not really implemented. I can see that LeanStructArray is probably a future TODO, but what about LeanMPZ? It seems that this is supposed to mean a GMP object. Is that also a future TODO?

[Mario Carneiro]

mpz is definitely a thing, try looking at the olean for def foo := 100000000000000000 if you want to see one