Literals

See the official user manual for the most up-to-date version of the information on this page.

TOC

Examples:

 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."

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.