See the official user manual for the most up-to-date version of the information on this page.
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."
A sequence of digits represents a natural number.
A character literal is given by
where c is any character except backslash or single-quote.
The backslash literal is written
'\\' and the single-quote literal
A string literal is given by
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.