

Part 1 Destring() - Removing Elements from the String Destring() removes an element from a string, i.e. "destrings" it. The element is then becomes an instance of it's type. You can only destring one element at a time. For example, if we have a string <x> with one element x in it, then we can do the following:
This effectively removes the element from the string, and it becomes an element x of type T.
|
||||