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.