See the official user manual for the most up-to-date version of the information on this page.
Numbers
A sequence of digits represents a natural number.
Characters
A character literal is given by
'
c'
where c is any character except backslash or single-quote.
The backslash literal is written '\\'
and the single-quote literal '\''
.
Strings
A string literal is given by
"
s"
where s is a sequence of characters, some of which may be escaped.
A non-escaped character is any Unicode character except backslash or double-quote.
An escaped character, and what it denotes, is listed below.
Escape Sequence | Meaning |
\\ | backslash |
\" | double-quote |
\n | newline |
\r | carriage return |
\t | tab |
Example
module Literals where open import Data.Nat open import Data.Char open import Data.String n42 : ℕ n42 = 42 z : ℕ z = 0 c : Char c = 'c' backslash : Char backslash = '\\' Hello : String Hello = "Hello, World!" s : String s = "This is a \"String\" containing two newlines\nand two double quotes."
Page last modified on December 14, 2018, at 03:40 pm
Powered by
PmWiki