Warning, file /frameworks/syntax-highlighting/autotests/html/test.agda.dark.html was not indexed or was modified since last indexation (in which case cross-reference links may be missing, inaccurate or erroneous).
0001 <!DOCTYPE html> 0002 <html><head> 0003 <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/> 0004 <title>test.agda</title> 0005 <meta name="generator" content="KF5::SyntaxHighlighting - Definition (Agda) - Theme (Breeze Dark)"/> 0006 </head><body style="background-color:#232629;color:#cfcfc2"><pre> 0007 <span style="color:#7a7c7d;">-- Agda Sample File</span> 0008 <span style="color:#7a7c7d;">-- https://github.com/agda/agda/blob/master/examples/syntax/highlighting/Test.agda</span> 0009 0010 <span style="color:#7a7c7d;">-- This test file currently lacks module-related stuff.</span> 0011 0012 <span style="color:#7a7c7d;">{- Nested</span> 0013 <span style="color:#7a7c7d;"> {- comment. -} -}</span> 0014 0015 <span style="font-weight:bold;">module</span> Test <span style="font-weight:bold;">where</span> 0016 0017 <span style="font-weight:bold;">infix</span> <span style="color:#f67400;">12</span> <span style="color:#27ae60;">_</span>! 0018 <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> 0019 <span style="font-weight:bold;">infixr</span> <span style="color:#f67400;">2</span> -<span style="color:#27ae60;">_</span> 0020 0021 <span style="font-weight:bold;">postulate</span> x <span style="color:#27ae60;">:</span> <span style="color:#2980b9;">Set</span> 0022 0023 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> 0024 f <span style="color:#27ae60;">_</span>*<span style="color:#27ae60;">_</span> <span style="color:#27ae60;">=</span> x * x 0025 0026 <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> 0027 zero <span style="color:#27ae60;">:</span> ℕ 0028 suc <span style="color:#27ae60;">:</span> ℕ <span style="color:#27ae60;">-></span> ℕ 0029 0030 <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> ℕ 0031 zero + n <span style="color:#27ae60;">=</span> n 0032 suc m + n <span style="color:#27ae60;">=</span> suc <span style="color:#27ae60;">(</span>m + n<span style="color:#27ae60;">)</span> 0033 0034 <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> ℕ 0035 0036 -<span style="color:#27ae60;">_</span> <span style="color:#27ae60;">:</span> ℕ <span style="color:#27ae60;">-></span> ℕ 0037 - n <span style="color:#27ae60;">=</span> n 0038 0039 <span style="color:#27ae60;">_</span>! <span style="color:#27ae60;">:</span> ℕ <span style="color:#27ae60;">-></span> ℕ 0040 zero ! <span style="color:#27ae60;">=</span> suc zero 0041 suc n ! <span style="color:#27ae60;">=</span> n - n ! 0042 0043 <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> 0044 <span style="font-weight:bold;">field</span> 0045 refl <span style="color:#27ae60;">:</span> <span style="font-weight:bold;">forall</span> x <span style="color:#27ae60;">-></span> x ≈ x 0046 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 0047 <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 0048 0049 <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> 0050 refl <span style="color:#27ae60;">:</span> x ≡ x 0051 0052 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> 0053 <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 0054 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 0055 0056 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> 0057 Equiv-≡ <span style="color:#27ae60;">{</span>a<span style="color:#27ae60;">}</span> <span style="color:#27ae60;">=</span> 0058 <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 0059 <span style="color:#27ae60;">;</span> sym <span style="color:#27ae60;">=</span> sym 0060 <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> 0061 <span style="color:#27ae60;">}</span> 0062 <span style="font-weight:bold;">where</span> 0063 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 0064 sym refl <span style="color:#27ae60;">=</span> refl 0065 0066 <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 0067 refl `trans` refl <span style="color:#27ae60;">=</span> refl 0068 0069 <span style="font-weight:bold;">postulate</span> 0070 String <span style="color:#27ae60;">:</span> <span style="color:#2980b9;">Set</span> 0071 Char <span style="color:#27ae60;">:</span> <span style="color:#2980b9;">Set</span> 0072 Float <span style="color:#27ae60;">:</span> <span style="color:#2980b9;">Set</span> 0073 0074 <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> 0075 pos <span style="color:#27ae60;">:</span> ℕ <span style="color:#27ae60;">→</span> Int 0076 negsuc <span style="color:#27ae60;">:</span> ℕ <span style="color:#27ae60;">→</span> Int 0077 0078 <span style="color:#27ae60;">{-# BUILTIN STRING String #-}</span> 0079 <span style="color:#27ae60;">{-# BUILTIN CHAR Char #-}</span> 0080 <span style="color:#27ae60;">{-# BUILTIN FLOAT Float #-}</span> 0081 0082 <span style="color:#27ae60;">{-# BUILTIN NATURAL ℕ #-}</span> 0083 0084 <span style="color:#27ae60;">{-# BUILTIN INTEGER Int #-}</span> 0085 <span style="color:#27ae60;">{-# BUILTIN INTEGERPOS pos #-}</span> 0086 <span style="color:#27ae60;">{-# BUILTIN INTEGERNEGSUC negsuc #-}</span> 0087 0088 <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> 0089 [] <span style="color:#27ae60;">:</span> [ a ] 0090 <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 ] 0091 0092 <span style="color:#27ae60;">{-# BUILTIN LIST [_] #-}</span> 0093 <span style="color:#27ae60;">{-# BUILTIN NIL [] #-}</span> 0094 <span style="color:#27ae60;">{-# BUILTIN CONS _∷_ #-}</span> 0095 0096 <span style="font-weight:bold;">primitive</span> 0097 primStringToList <span style="color:#27ae60;">:</span> String <span style="color:#27ae60;">-></span> [ Char ] 0098 0099 string <span style="color:#27ae60;">:</span> [ Char ] 0100 string <span style="color:#27ae60;">=</span> primStringToList <span style="color:#f44f4f;">"∃ apa"</span> 0101 0102 char <span style="color:#27ae60;">:</span> Char 0103 char <span style="color:#27ae60;">=</span> <span style="color:#3daee9;">'∀'</span> 0104 0105 anotherString <span style="color:#27ae60;">:</span> String 0106 anotherString <span style="color:#27ae60;">=</span> <span style="color:#f44f4f;">"¬ be\</span> 0107 <span style="color:#f44f4f;"> \pa"</span> 0108 0109 nat <span style="color:#27ae60;">:</span> ℕ 0110 nat <span style="color:#27ae60;">=</span> <span style="color:#f67400;">45</span> 0111 0112 float <span style="color:#27ae60;">:</span> Float 0113 float <span style="color:#27ae60;">=</span> <span style="color:#f67400;">45.0e-37</span> 0114 0115 <span style="color:#7a7c7d;">-- Testing qualified names.</span> 0116 0117 <span style="font-weight:bold;">open</span> <span style="font-weight:bold;">import</span> Test 0118 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> 0119 </pre></body></html>