stringSyntax = HOLinML