Extractor to recognise the string str.cons function.
Extractor to recognise the string str.cons function.
Extractor to recognise the string str.empty function.
Extractor to recognise the string str.empty function.
(Since version ) see corresponding Javadoc for more information.