Recently I were viewing Paxos implementation in https://github.com/tlaplus/Examples/blob/master/specifications/Paxos/Paxos.tla
, in which there is a statement as
`Ballot == Nat`.
Since `Nat` is non-enumerable, the toolbox would raise an error if I didn't override `Ballot`.
So I am wondering what the reasons are that to design `Ballot` in this way. Why not just setting it something like `Ballot == 0..10` in the first place?