Add ℕ, ℤ, and ℝ to the standard modules

[ahelwer]

When Unicode support was merged earlier this year these were kept out of the standard modules out of stability considerations. This means Unicode users must write specs like:

---- MODULE Demo ----
EXTENDS Naturals
ℕ == Nat
\* Rest of spec using ℕ
====

if they want to use ℕ in their specs without generating a symbol-not-found error. If Apalache is going to pull in SANY to support Unicode itself (see apalache-mc/apalache#2995) perhaps these definitions should be added to the standard modules.

There is one issue that complicates this beyond simply defining ℕ == Nat in Naturals.tla, and that is definition overrides. It is very, very common for users to override the definitions of Nat, Int, and Real with finite sets. I foresee the following issues:

1. The model configuration parser does not support Unicode so would have to be modified so users can define override values for ℕ, ℤ, and ℝ instead of having to use Nat, Int, and Real.
2. If users override the definitions of ℕ, ℤ, and ℝ, then we might also want to override the definitions of Nat, Int, and Real automatically so they don't have to do it twice.

Arguably we shouldn't actually do 2 since no other definitions in TLA+ work this way; operator synonyms like <= and \leq do work this way, but Nat, Int, and Real are definitions, not operators. However, these definitions are being given special treatment with the unique symbols ℕ, ℤ, and ℝ so perhaps it makes sense to make the synonym official.

[lemmy]

It needs to be verified whether the Toolbox's model editor properly supports Unicode symbols, such as those used in definition overrides.

[Calvin-L]

Wasn't there also some question about TLAPS support? (Perhaps I'm misremembering.)

EDIT: Yes, it was mentioned here: #896 (comment)
We probably shouldn't make this change until TLAPS supports it.

[lemmy]

#911 (comment) is a related Unicode issue that suggests we should tread carefully here.