-- 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.ℕ}