1-- Agda Sample File
2-- https://github.com/agda/agda/blob/master/examples/syntax/highlighting/Test.agda
3
4-- This test file currently lacks module-related stuff.
5
6{- Nested
7   {- comment. -} -}
8
9module Test where
10
11infix  12 _!
12infixl  7 _+_ _-_
13infixr  2 -_
14
15postulate x : Set
16
17f : (Set -> Set -> Set) -> Set
18f _*_ = x * x
19
20data ℕ : Set where
21  zero : ℕ
22  suc  : ℕ -> ℕ
23
24_+_ : ℕ -> ℕ -> ℕ
25zero  + n = n
26suc m + n = suc (m + n)
27
28postulate _-_ : ℕ -> ℕ -> ℕ
29
30-_ : ℕ -> ℕ
31- n = n
32
33_! : ℕ -> ℕ
34zero  ! = suc zero
35suc n ! = n - n !
36
37record Equiv {a : Set} (_≈_ : a -> a -> Set) : Set where
38  field
39    refl      : forall x       -> x ≈ x
40    sym       : {x y : a}      -> x ≈ y -> y ≈ x
41    _`trans`_ : forall {x y z} -> x ≈ y -> y ≈ z -> x ≈ z
42
43data _≡_ {a : Set} (x : a) : a -> Set where
44  refl : x ≡ x
45
46subst : forall {a x y} ->
47  (P : a -> Set) -> x ≡ y -> P x -> P y
48subst {x = x} .{y = x} _ refl p = p
49
50Equiv-≡ : forall {a} -> Equiv {a} _≡_
51Equiv-≡ {a} =
52  record { refl      = \_ -> refl
53         ; sym       = sym
54         ; _`trans`_ = _`trans`_
55         }
56  where
57  sym : {x y : a} -> x ≡ y -> y ≡ x
58  sym refl = refl
59
60  _`trans`_ : {x y z : a} -> x ≡ y -> y ≡ z -> x ≡ z
61  refl `trans` refl = refl
62
63postulate
64  String : Set
65  Char   : Set
66  Float  : Set
67
68data Int : Set where
69  pos    : ℕ → Int
70  negsuc : ℕ → Int
71
72{-# BUILTIN STRING  String #-}
73{-# BUILTIN CHAR    Char   #-}
74{-# BUILTIN FLOAT   Float  #-}
75
76{-# BUILTIN NATURAL ℕ      #-}
77
78{-# BUILTIN INTEGER       Int    #-}
79{-# BUILTIN INTEGERPOS    pos    #-}
80{-# BUILTIN INTEGERNEGSUC negsuc #-}
81
82data [_] (a : Set) : Set where
83  []  : [ a ]
84  _∷_ : a -> [ a ] -> [ a ]
85
86{-# BUILTIN LIST [_] #-}
87{-# BUILTIN NIL  []  #-}
88{-# BUILTIN CONS _∷_ #-}
89
90primitive
91  primStringToList : String -> [ Char ]
92
93string : [ Char ]
94string = primStringToList "∃ apa"
95
96char : Char
97char = '∀'
98
99anotherString : String
100anotherString = "¬ be\
101    \pa"
102
103nat : ℕ
104nat = 45
105
106float : Float
107float = 45.0e-37
108
109-- Testing qualified names.
110
111open import Test
112Eq = Test.Equiv {Test.ℕ}
113