1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
<indentfold>-- Agda Sample File
-- https://github.com/agda/agda/blob/master/examples/syntax/highlighting/Test.agda
-- This test file currently lacks module-related stuff.
</indentfold><beginfold id='1'>{-</beginfold id='1'> Nested
<indentfold> <beginfold id='1'>{-</beginfold id='1'> comment. <endfold id='1'>-}</endfold id='1'> <endfold id='1'>-}</endfold id='1'>
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.ℕ}
|
