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
113
114
115
116
117
118
119
|
<!DOCTYPE html>
<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
<title>test.agda</title>
<meta name="generator" content="KF5::SyntaxHighlighting - Definition (Agda) - Theme (Breeze Dark)"/>
</head><body style="background-color:#232629;color:#cfcfc2"><pre>
<span style="color:#7a7c7d">-- Agda Sample File</span>
<span style="color:#7a7c7d">-- https://github.com/agda/agda/blob/master/examples/syntax/highlighting/Test.agda</span>
<span style="color:#7a7c7d">-- This test file currently lacks module-related stuff.</span>
<span style="color:#7a7c7d">{- Nested</span>
<span style="color:#7a7c7d"> {- comment. -} -}</span>
<span style="font-weight:bold">module</span> Test <span style="font-weight:bold">where</span>
<span style="font-weight:bold">infix</span> <span style="color:#f67400">12</span> <span style="color:#27ae60">_</span>!
<span style="font-weight:bold">infixl</span> <span style="color:#f67400">7</span> <span style="color:#27ae60">_</span>+<span style="color:#27ae60">_</span> <span style="color:#27ae60">_</span>-<span style="color:#27ae60">_</span>
<span style="font-weight:bold">infixr</span> <span style="color:#f67400">2</span> -<span style="color:#27ae60">_</span>
<span style="font-weight:bold">postulate</span> x <span style="color:#27ae60">:</span> <span style="color:#2980b9">Set</span>
f <span style="color:#27ae60">:</span> <span style="color:#27ae60">(</span><span style="color:#2980b9">Set</span> <span style="color:#27ae60">-></span> <span style="color:#2980b9">Set</span> <span style="color:#27ae60">-></span> <span style="color:#2980b9">Set</span><span style="color:#27ae60">)</span> <span style="color:#27ae60">-></span> <span style="color:#2980b9">Set</span>
f <span style="color:#27ae60">_</span>*<span style="color:#27ae60">_</span> <span style="color:#27ae60">=</span> x * x
<span style="font-weight:bold">data</span> ℕ <span style="color:#27ae60">:</span> <span style="color:#2980b9">Set</span> <span style="font-weight:bold">where</span>
zero <span style="color:#27ae60">:</span> ℕ
suc <span style="color:#27ae60">:</span> ℕ <span style="color:#27ae60">-></span> ℕ
<span style="color:#27ae60">_</span>+<span style="color:#27ae60">_</span> <span style="color:#27ae60">:</span> ℕ <span style="color:#27ae60">-></span> ℕ <span style="color:#27ae60">-></span> ℕ
zero + n <span style="color:#27ae60">=</span> n
suc m + n <span style="color:#27ae60">=</span> suc <span style="color:#27ae60">(</span>m + n<span style="color:#27ae60">)</span>
<span style="font-weight:bold">postulate</span> <span style="color:#27ae60">_</span>-<span style="color:#27ae60">_</span> <span style="color:#27ae60">:</span> ℕ <span style="color:#27ae60">-></span> ℕ <span style="color:#27ae60">-></span> ℕ
-<span style="color:#27ae60">_</span> <span style="color:#27ae60">:</span> ℕ <span style="color:#27ae60">-></span> ℕ
- n <span style="color:#27ae60">=</span> n
<span style="color:#27ae60">_</span>! <span style="color:#27ae60">:</span> ℕ <span style="color:#27ae60">-></span> ℕ
zero ! <span style="color:#27ae60">=</span> suc zero
suc n ! <span style="color:#27ae60">=</span> n - n !
<span style="font-weight:bold">record</span> Equiv <span style="color:#27ae60">{</span>a <span style="color:#27ae60">:</span> <span style="color:#2980b9">Set</span><span style="color:#27ae60">}</span> <span style="color:#27ae60">(_</span>≈<span style="color:#27ae60">_</span> <span style="color:#27ae60">:</span> a <span style="color:#27ae60">-></span> a <span style="color:#27ae60">-></span> <span style="color:#2980b9">Set</span><span style="color:#27ae60">)</span> <span style="color:#27ae60">:</span> <span style="color:#2980b9">Set</span> <span style="font-weight:bold">where</span>
<span style="font-weight:bold">field</span>
refl <span style="color:#27ae60">:</span> <span style="font-weight:bold">forall</span> x <span style="color:#27ae60">-></span> x ≈ x
sym <span style="color:#27ae60">:</span> <span style="color:#27ae60">{</span>x y <span style="color:#27ae60">:</span> a<span style="color:#27ae60">}</span> <span style="color:#27ae60">-></span> x ≈ y <span style="color:#27ae60">-></span> y ≈ x
<span style="color:#27ae60">_</span>`trans`<span style="color:#27ae60">_</span> <span style="color:#27ae60">:</span> <span style="font-weight:bold">forall</span> <span style="color:#27ae60">{</span>x y z<span style="color:#27ae60">}</span> <span style="color:#27ae60">-></span> x ≈ y <span style="color:#27ae60">-></span> y ≈ z <span style="color:#27ae60">-></span> x ≈ z
<span style="font-weight:bold">data</span> <span style="color:#27ae60">_</span>≡<span style="color:#27ae60">_</span> <span style="color:#27ae60">{</span>a <span style="color:#27ae60">:</span> <span style="color:#2980b9">Set</span><span style="color:#27ae60">}</span> <span style="color:#27ae60">(</span>x <span style="color:#27ae60">:</span> a<span style="color:#27ae60">)</span> <span style="color:#27ae60">:</span> a <span style="color:#27ae60">-></span> <span style="color:#2980b9">Set</span> <span style="font-weight:bold">where</span>
refl <span style="color:#27ae60">:</span> x ≡ x
subst <span style="color:#27ae60">:</span> <span style="font-weight:bold">forall</span> <span style="color:#27ae60">{</span>a x y<span style="color:#27ae60">}</span> <span style="color:#27ae60">-></span>
<span style="color:#27ae60">(</span>P <span style="color:#27ae60">:</span> a <span style="color:#27ae60">-></span> <span style="color:#2980b9">Set</span><span style="color:#27ae60">)</span> <span style="color:#27ae60">-></span> x ≡ y <span style="color:#27ae60">-></span> P x <span style="color:#27ae60">-></span> P y
subst <span style="color:#27ae60">{</span>x <span style="color:#27ae60">=</span> x<span style="color:#27ae60">}</span> <span style="color:#27ae60">.{</span>y <span style="color:#27ae60">=</span> x<span style="color:#27ae60">}</span> <span style="color:#27ae60">_</span> refl p <span style="color:#27ae60">=</span> p
Equiv-≡ <span style="color:#27ae60">:</span> <span style="font-weight:bold">forall</span> <span style="color:#27ae60">{</span>a<span style="color:#27ae60">}</span> <span style="color:#27ae60">-></span> Equiv <span style="color:#27ae60">{</span>a<span style="color:#27ae60">}</span> <span style="color:#27ae60">_</span>≡<span style="color:#27ae60">_</span>
Equiv-≡ <span style="color:#27ae60">{</span>a<span style="color:#27ae60">}</span> <span style="color:#27ae60">=</span>
<span style="font-weight:bold">record</span> <span style="color:#27ae60">{</span> refl <span style="color:#27ae60">=</span> <span style="color:#27ae60">\_</span> <span style="color:#27ae60">-></span> refl
<span style="color:#27ae60">;</span> sym <span style="color:#27ae60">=</span> sym
<span style="color:#27ae60">;</span> <span style="color:#27ae60">_</span>`trans`<span style="color:#27ae60">_</span> <span style="color:#27ae60">=</span> <span style="color:#27ae60">_</span>`trans`<span style="color:#27ae60">_</span>
<span style="color:#27ae60">}</span>
<span style="font-weight:bold">where</span>
sym <span style="color:#27ae60">:</span> <span style="color:#27ae60">{</span>x y <span style="color:#27ae60">:</span> a<span style="color:#27ae60">}</span> <span style="color:#27ae60">-></span> x ≡ y <span style="color:#27ae60">-></span> y ≡ x
sym refl <span style="color:#27ae60">=</span> refl
<span style="color:#27ae60">_</span>`trans`<span style="color:#27ae60">_</span> <span style="color:#27ae60">:</span> <span style="color:#27ae60">{</span>x y z <span style="color:#27ae60">:</span> a<span style="color:#27ae60">}</span> <span style="color:#27ae60">-></span> x ≡ y <span style="color:#27ae60">-></span> y ≡ z <span style="color:#27ae60">-></span> x ≡ z
refl `trans` refl <span style="color:#27ae60">=</span> refl
<span style="font-weight:bold">postulate</span>
String <span style="color:#27ae60">:</span> <span style="color:#2980b9">Set</span>
Char <span style="color:#27ae60">:</span> <span style="color:#2980b9">Set</span>
Float <span style="color:#27ae60">:</span> <span style="color:#2980b9">Set</span>
<span style="font-weight:bold">data</span> Int <span style="color:#27ae60">:</span> <span style="color:#2980b9">Set</span> <span style="font-weight:bold">where</span>
pos <span style="color:#27ae60">:</span> ℕ <span style="color:#27ae60">→</span> Int
negsuc <span style="color:#27ae60">:</span> ℕ <span style="color:#27ae60">→</span> Int
<span style="color:#27ae60">{-# BUILTIN STRING String #-}</span>
<span style="color:#27ae60">{-# BUILTIN CHAR Char #-}</span>
<span style="color:#27ae60">{-# BUILTIN FLOAT Float #-}</span>
<span style="color:#27ae60">{-# BUILTIN NATURAL ℕ #-}</span>
<span style="color:#27ae60">{-# BUILTIN INTEGER Int #-}</span>
<span style="color:#27ae60">{-# BUILTIN INTEGERPOS pos #-}</span>
<span style="color:#27ae60">{-# BUILTIN INTEGERNEGSUC negsuc #-}</span>
<span style="font-weight:bold">data</span> [<span style="color:#27ae60">_</span>] <span style="color:#27ae60">(</span>a <span style="color:#27ae60">:</span> <span style="color:#2980b9">Set</span><span style="color:#27ae60">)</span> <span style="color:#27ae60">:</span> <span style="color:#2980b9">Set</span> <span style="font-weight:bold">where</span>
[] <span style="color:#27ae60">:</span> [ a ]
<span style="color:#27ae60">_</span>∷<span style="color:#27ae60">_</span> <span style="color:#27ae60">:</span> a <span style="color:#27ae60">-></span> [ a ] <span style="color:#27ae60">-></span> [ a ]
<span style="color:#27ae60">{-# BUILTIN LIST [_] #-}</span>
<span style="color:#27ae60">{-# BUILTIN NIL [] #-}</span>
<span style="color:#27ae60">{-# BUILTIN CONS _∷_ #-}</span>
<span style="font-weight:bold">primitive</span>
primStringToList <span style="color:#27ae60">:</span> String <span style="color:#27ae60">-></span> [ Char ]
string <span style="color:#27ae60">:</span> [ Char ]
string <span style="color:#27ae60">=</span> primStringToList <span style="color:#f44f4f">"∃ apa"</span>
char <span style="color:#27ae60">:</span> Char
char <span style="color:#27ae60">=</span> <span style="color:#3daee9">'∀'</span>
anotherString <span style="color:#27ae60">:</span> String
anotherString <span style="color:#27ae60">=</span> <span style="color:#f44f4f">"¬ be\</span>
<span style="color:#f44f4f"> \pa"</span>
nat <span style="color:#27ae60">:</span> ℕ
nat <span style="color:#27ae60">=</span> <span style="color:#f67400">45</span>
float <span style="color:#27ae60">:</span> Float
float <span style="color:#27ae60">=</span> <span style="color:#f67400">45.0e-37</span>
<span style="color:#7a7c7d">-- Testing qualified names.</span>
<span style="font-weight:bold">open</span> <span style="font-weight:bold">import</span> Test
Eq <span style="color:#27ae60">=</span> Test<span style="color:#27ae60">.</span>Equiv <span style="color:#27ae60">{</span>Test<span style="color:#27ae60">.</span>ℕ<span style="color:#27ae60">}</span>
</pre></body></html>
|
