```-- Agda Sample File
-- https://github.com/agda/agda/blob/master/examples/syntax/highlighting/Test.agda

-- This test file currently lacks module-related stuff.

{- Nested
{- comment. -} -}

module Test where

infix  12 _!
infixl  7 _+_ _-_
infixr  2 -_

postulate x : Set

f : (Set -> Set -> Set) -> Set
f _*_ = x * x

data ℕ : Set where
zero : ℕ
suc  : ℕ -> ℕ

_+_ : ℕ -> ℕ -> ℕ
zero  + n = n
suc m + n = suc (m + n)

postulate _-_ : ℕ -> ℕ -> ℕ

-_ : ℕ -> ℕ
- n = n

_! : ℕ -> ℕ
zero  ! = suc zero
suc n ! = n - n !

record Equiv {a : Set} (_≈_ : a -> a -> Set) : Set where
field
refl      : forall x       -> x ≈ x
sym       : {x y : a}      -> x ≈ y -> y ≈ x
_`trans`_ : forall {x y z} -> x ≈ y -> y ≈ z -> x ≈ z

data _≡_ {a : Set} (x : a) : a -> Set where
refl : x ≡ x

subst : forall {a x y} ->
(P : a -> Set) -> x ≡ y -> P x -> P y
subst {x = x} .{y = x} _ refl p = p

Equiv-≡ : forall {a} -> Equiv {a} _≡_
Equiv-≡ {a} =
record { refl      = \_ -> refl
; sym       = sym
; _`trans`_ = _`trans`_
}
where
sym : {x y : a} -> x ≡ y -> y ≡ x
sym refl = refl

_`trans`_ : {x y z : a} -> x ≡ y -> y ≡ z -> x ≡ z
refl `trans` refl = refl

postulate
String : Set
Char   : Set
Float  : Set

data Int : Set where
pos    : ℕ → Int
negsuc : ℕ → Int

{-# BUILTIN STRING  String #-}
{-# BUILTIN CHAR    Char   #-}
{-# BUILTIN FLOAT   Float  #-}

{-# BUILTIN NATURAL ℕ      #-}

{-# BUILTIN INTEGER       Int    #-}
{-# BUILTIN INTEGERPOS    pos    #-}
{-# BUILTIN INTEGERNEGSUC negsuc #-}

data [_] (a : Set) : Set where
[]  : [ a ]
_∷_ : a -> [ a ] -> [ a ]

{-# BUILTIN LIST [_] #-}
{-# BUILTIN NIL  []  #-}
{-# BUILTIN CONS _∷_ #-}

primitive
primStringToList : String -> [ Char ]

string : [ Char ]
string = primStringToList "∃ apa"

char : Char
char = '∀'

anotherString : String
anotherString = "¬ be\
\pa"

nat : ℕ
nat = 45

float : Float
float = 45.0e-37

-- Testing qualified names.

open import Test
Eq = Test.Equiv {Test.ℕ}
```