How to convert number to string in TLA+

Effectively, I want to build a {"1", "2", "3", ..., "N"} set from 1..N set. How do I convert numbers to strings?

Solution

The TLC module provides a ToString operator.

Proving correctness of Matrix Addition
accessing members of constrained type parameters in Dafny
Issues with converting 2D matrix indices to 1D array index
Copy a singly linked list with Frama-C
Turn `P(?x)` into `exists x,P(x)` to give different instantiations for different subgoals in Coq
How to add an element to a total function while making sure no other mapping to this element exists?
WP Plugin: Why does the following simplified code fail to verify
How to create a constant reference to an object in Dafny
Alloy does not find a solution (instance) for my specification
How do I check if the result of symTake is equal to a concrete list?
How to revers a seq relation in Alloy
Formal verification of state machine with SymbiYosys not giving expected results
How do you prove termination of a recursive list length?
Dafny issue modifying array member of class
How to verify C functions with array parameters using Isabelle
How to prove a = b → a + 1 = b + 1 in lean?
Can't compile Hello World in F*
How to prove properties of non-linear operators involved in LEB128 algorithm in Dafny?
How to capture a change in an element of an array in TLA+
Dafny method will not verify
Dafny Method to find Max fails to verify
Dafny: How to call 'verifcationLogger:csv'?
Checked Non-Terminating Recursive Def?
Why Does Rewrite Fail to Bind?
Dafny: Generic method on a base type and a subset type?
Dafny: Library of common operations such as partition?
Trying for a little Dafny proof about "touching" integers
Dafny: Want to show that a sequence of sets == the set of the sequence (corrected)
Dafny: Method times out when unrelated conditions are added
In Dafny, show that a sequence of unique elements has the same size as the set of the same elements