Feature Request: Standard Library implementation of Char and String?

[gjveltink]

I am currently developing a larger specification for a real-life industrial production system, which we use in our education. One of the objectives of this specification is to incorporate the "Asset Administration Shell" standard for Industrie 4.0 components (IEC TR 62794 & IEC 62832 Digital Factory). This standard heavily relies on common representations of "strings".

To faithfully adhere to the standard, I had to introduce a custom sort "String" While this is technically possible, the implementation becomes quite cumbersome—particularly when it comes to representing digits within strings.

% -----------------------------------------------------------------------------------------------------------------------
%
% self-defined characters and strings
%

sort Char = struct
	a | b | c | d | e | f | g | h | i | j | k | l | m | n | o | p | q | r | s | t | u | v | w | x | y | z
	| A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z
        | _0 | _1 | _2 | _3 | _4 | _5 | _6 | _7 | _8 | _9 
;

sort String = List(Char);

% example usage
map mCRL2: String;
eqn mCRL2 = [m,C,R,L,_2];

Unfortunately, this scheme also eliminates the possibility of using single-character variables throughout the rest of the specification, which can be a nuisance as well.

Therefore, I would strongly advocate for the inclusion of Characters and Strings in the standard library of data types in a future version of mCRL2.
This addition would not only enhance the functionality of the language but also make it more appealing to my students.
In fact, I often encounter discussions during lectures where I have to justify the absence of these fundamental data types in mCRL2.