lean4-htt/tests/lean/char_lits.lean
Gabriel Ebner 16fb5ade58 fix(library/string): correctly escape non-printable characters
This also fixes a compiler warning on ARM, where `0 <= c` is always
true.
2017-06-23 20:39:41 +02:00

15 lines
323 B
Text

import system.io
open io
#check 'a'
#eval 'a'
#eval '\n'
#eval '\\'
variable [io.interface]
#eval put_str ("aaa".str '\\')
#eval put_str $ repr '\n'
#eval put_str $ string.singleton '\n'
#eval put_str ("aaa".str '\'')
#check ['\x7f', '\x00', '\x11', '\xff']
-- ^^ all characters should be pretty-printed using \x escapes