String generator
GENERATOR String (TYPE Elementtype,
OPERATORS
Mkstring : Elementtype -> String ;
Length : String -> Integer;
First : String -> Elementtype;
Last : String -> Elementtype;
// : String , String -> String;
Substring : String , Integer, Integer -> String ;
Extract! : String , Integer -> Elementtype;
Modify! : String , Integer, Elementtype -> String ;