[tlaplus] The Naturals module

["'Ugur Yavuz' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>]

In Specifying Systems, the Naturals module defines natural numbers as an arbitrary set with a constant zero and a successor function satisfying the usual Peano axioms. This is done across a number of modules, namely Peano, ProtoReals and then Naturals. 

It seems that this original formulation was later replaced by a Naturals module containing only placeholder definitions, with the expectation that TLA⁺ tools (e.g., TLC, TLAPS) would provide their own implementations of natural number operators.

Could anyone comment on this change? And more generally, how should one think about the Naturals module in TLA⁺ today?

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/07de996d-fc76-40ee-bb40-6ed5b17050c6n%40googlegroups.com.