File indexing completed on 2024-05-12 04:02:09
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 Light)"/> 0006 </head><body style="background-color:#ffffff;color:#1f1c1b"><pre> 0007 <span style="color:#898887">-- Agda Sample File</span> 0008 <span style="color:#898887">-- https://github.com/agda/agda/blob/master/examples/syntax/highlighting/Test.agda</span> 0009 0010 <span style="color:#898887">-- This test file currently lacks module-related stuff.</span> 0011 0012 <span style="color:#898887">{- Nested</span> 0013 <span style="color:#898887"> {- 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:#b08000">12</span> <span style="color:#006e28">_</span>! 0018 <span style="font-weight:bold">infixl</span> <span style="color:#b08000">7</span> <span style="color:#006e28">_</span>+<span style="color:#006e28">_</span> <span style="color:#006e28">_</span>-<span style="color:#006e28">_</span> 0019 <span style="font-weight:bold">infixr</span> <span style="color:#b08000">2</span> -<span style="color:#006e28">_</span> 0020 0021 <span style="font-weight:bold">postulate</span> x <span style="color:#006e28">:</span> <span style="color:#0057ae">Set</span> 0022 0023 f <span style="color:#006e28">:</span> <span style="color:#006e28">(</span><span style="color:#0057ae">Set</span> <span style="color:#006e28">-></span> <span style="color:#0057ae">Set</span> <span style="color:#006e28">-></span> <span style="color:#0057ae">Set</span><span style="color:#006e28">)</span> <span style="color:#006e28">-></span> <span style="color:#0057ae">Set</span> 0024 f <span style="color:#006e28">_</span>*<span style="color:#006e28">_</span> <span style="color:#006e28">=</span> x * x 0025 0026 <span style="font-weight:bold">data</span> ℕ <span style="color:#006e28">:</span> <span style="color:#0057ae">Set</span> <span style="font-weight:bold">where</span> 0027 zero <span style="color:#006e28">:</span> ℕ 0028 suc <span style="color:#006e28">:</span> ℕ <span style="color:#006e28">-></span> ℕ 0029 0030 <span style="color:#006e28">_</span>+<span style="color:#006e28">_</span> <span style="color:#006e28">:</span> ℕ <span style="color:#006e28">-></span> ℕ <span style="color:#006e28">-></span> ℕ 0031 zero + n <span style="color:#006e28">=</span> n 0032 suc m + n <span style="color:#006e28">=</span> suc <span style="color:#006e28">(</span>m + n<span style="color:#006e28">)</span> 0033 0034 <span style="font-weight:bold">postulate</span> <span style="color:#006e28">_</span>-<span style="color:#006e28">_</span> <span style="color:#006e28">:</span> ℕ <span style="color:#006e28">-></span> ℕ <span style="color:#006e28">-></span> ℕ 0035 0036 -<span style="color:#006e28">_</span> <span style="color:#006e28">:</span> ℕ <span style="color:#006e28">-></span> ℕ 0037 - n <span style="color:#006e28">=</span> n 0038 0039 <span style="color:#006e28">_</span>! <span style="color:#006e28">:</span> ℕ <span style="color:#006e28">-></span> ℕ 0040 zero ! <span style="color:#006e28">=</span> suc zero 0041 suc n ! <span style="color:#006e28">=</span> n - n ! 0042 0043 <span style="font-weight:bold">record</span> Equiv <span style="color:#006e28">{</span>a <span style="color:#006e28">:</span> <span style="color:#0057ae">Set</span><span style="color:#006e28">}</span> <span style="color:#006e28">(_</span>≈<span style="color:#006e28">_</span> <span style="color:#006e28">:</span> a <span style="color:#006e28">-></span> a <span style="color:#006e28">-></span> <span style="color:#0057ae">Set</span><span style="color:#006e28">)</span> <span style="color:#006e28">:</span> <span style="color:#0057ae">Set</span> <span style="font-weight:bold">where</span> 0044 <span style="font-weight:bold">field</span> 0045 refl <span style="color:#006e28">:</span> <span style="font-weight:bold">forall</span> x <span style="color:#006e28">-></span> x ≈ x 0046 sym <span style="color:#006e28">:</span> <span style="color:#006e28">{</span>x y <span style="color:#006e28">:</span> a<span style="color:#006e28">}</span> <span style="color:#006e28">-></span> x ≈ y <span style="color:#006e28">-></span> y ≈ x 0047 <span style="color:#006e28">_</span>`trans`<span style="color:#006e28">_</span> <span style="color:#006e28">:</span> <span style="font-weight:bold">forall</span> <span style="color:#006e28">{</span>x y z<span style="color:#006e28">}</span> <span style="color:#006e28">-></span> x ≈ y <span style="color:#006e28">-></span> y ≈ z <span style="color:#006e28">-></span> x ≈ z 0048 0049 <span style="font-weight:bold">data</span> <span style="color:#006e28">_</span>≡<span style="color:#006e28">_</span> <span style="color:#006e28">{</span>a <span style="color:#006e28">:</span> <span style="color:#0057ae">Set</span><span style="color:#006e28">}</span> <span style="color:#006e28">(</span>x <span style="color:#006e28">:</span> a<span style="color:#006e28">)</span> <span style="color:#006e28">:</span> a <span style="color:#006e28">-></span> <span style="color:#0057ae">Set</span> <span style="font-weight:bold">where</span> 0050 refl <span style="color:#006e28">:</span> x ≡ x 0051 0052 subst <span style="color:#006e28">:</span> <span style="font-weight:bold">forall</span> <span style="color:#006e28">{</span>a x y<span style="color:#006e28">}</span> <span style="color:#006e28">-></span> 0053 <span style="color:#006e28">(</span>P <span style="color:#006e28">:</span> a <span style="color:#006e28">-></span> <span style="color:#0057ae">Set</span><span style="color:#006e28">)</span> <span style="color:#006e28">-></span> x ≡ y <span style="color:#006e28">-></span> P x <span style="color:#006e28">-></span> P y 0054 subst <span style="color:#006e28">{</span>x <span style="color:#006e28">=</span> x<span style="color:#006e28">}</span> <span style="color:#006e28">.{</span>y <span style="color:#006e28">=</span> x<span style="color:#006e28">}</span> <span style="color:#006e28">_</span> refl p <span style="color:#006e28">=</span> p 0055 0056 Equiv-≡ <span style="color:#006e28">:</span> <span style="font-weight:bold">forall</span> <span style="color:#006e28">{</span>a<span style="color:#006e28">}</span> <span style="color:#006e28">-></span> Equiv <span style="color:#006e28">{</span>a<span style="color:#006e28">}</span> <span style="color:#006e28">_</span>≡<span style="color:#006e28">_</span> 0057 Equiv-≡ <span style="color:#006e28">{</span>a<span style="color:#006e28">}</span> <span style="color:#006e28">=</span> 0058 <span style="font-weight:bold">record</span> <span style="color:#006e28">{</span> refl <span style="color:#006e28">=</span> <span style="color:#006e28">\_</span> <span style="color:#006e28">-></span> refl 0059 <span style="color:#006e28">;</span> sym <span style="color:#006e28">=</span> sym 0060 <span style="color:#006e28">;</span> <span style="color:#006e28">_</span>`trans`<span style="color:#006e28">_</span> <span style="color:#006e28">=</span> <span style="color:#006e28">_</span>`trans`<span style="color:#006e28">_</span> 0061 <span style="color:#006e28">}</span> 0062 <span style="font-weight:bold">where</span> 0063 sym <span style="color:#006e28">:</span> <span style="color:#006e28">{</span>x y <span style="color:#006e28">:</span> a<span style="color:#006e28">}</span> <span style="color:#006e28">-></span> x ≡ y <span style="color:#006e28">-></span> y ≡ x 0064 sym refl <span style="color:#006e28">=</span> refl 0065 0066 <span style="color:#006e28">_</span>`trans`<span style="color:#006e28">_</span> <span style="color:#006e28">:</span> <span style="color:#006e28">{</span>x y z <span style="color:#006e28">:</span> a<span style="color:#006e28">}</span> <span style="color:#006e28">-></span> x ≡ y <span style="color:#006e28">-></span> y ≡ z <span style="color:#006e28">-></span> x ≡ z 0067 refl `trans` refl <span style="color:#006e28">=</span> refl 0068 0069 <span style="font-weight:bold">postulate</span> 0070 String <span style="color:#006e28">:</span> <span style="color:#0057ae">Set</span> 0071 Char <span style="color:#006e28">:</span> <span style="color:#0057ae">Set</span> 0072 Float <span style="color:#006e28">:</span> <span style="color:#0057ae">Set</span> 0073 0074 <span style="font-weight:bold">data</span> Int <span style="color:#006e28">:</span> <span style="color:#0057ae">Set</span> <span style="font-weight:bold">where</span> 0075 pos <span style="color:#006e28">:</span> ℕ <span style="color:#006e28">→</span> Int 0076 negsuc <span style="color:#006e28">:</span> ℕ <span style="color:#006e28">→</span> Int 0077 0078 <span style="color:#006e28">{-# BUILTIN STRING String #-}</span> 0079 <span style="color:#006e28">{-# BUILTIN CHAR Char #-}</span> 0080 <span style="color:#006e28">{-# BUILTIN FLOAT Float #-}</span> 0081 0082 <span style="color:#006e28">{-# BUILTIN NATURAL ℕ #-}</span> 0083 0084 <span style="color:#006e28">{-# BUILTIN INTEGER Int #-}</span> 0085 <span style="color:#006e28">{-# BUILTIN INTEGERPOS pos #-}</span> 0086 <span style="color:#006e28">{-# BUILTIN INTEGERNEGSUC negsuc #-}</span> 0087 0088 <span style="font-weight:bold">data</span> [<span style="color:#006e28">_</span>] <span style="color:#006e28">(</span>a <span style="color:#006e28">:</span> <span style="color:#0057ae">Set</span><span style="color:#006e28">)</span> <span style="color:#006e28">:</span> <span style="color:#0057ae">Set</span> <span style="font-weight:bold">where</span> 0089 [] <span style="color:#006e28">:</span> [ a ] 0090 <span style="color:#006e28">_</span>∷<span style="color:#006e28">_</span> <span style="color:#006e28">:</span> a <span style="color:#006e28">-></span> [ a ] <span style="color:#006e28">-></span> [ a ] 0091 0092 <span style="color:#006e28">{-# BUILTIN LIST [_] #-}</span> 0093 <span style="color:#006e28">{-# BUILTIN NIL [] #-}</span> 0094 <span style="color:#006e28">{-# BUILTIN CONS _∷_ #-}</span> 0095 0096 <span style="font-weight:bold">primitive</span> 0097 primStringToList <span style="color:#006e28">:</span> String <span style="color:#006e28">-></span> [ Char ] 0098 0099 string <span style="color:#006e28">:</span> [ Char ] 0100 string <span style="color:#006e28">=</span> primStringToList <span style="color:#bf0303">"∃ apa"</span> 0101 0102 char <span style="color:#006e28">:</span> Char 0103 char <span style="color:#006e28">=</span> <span style="color:#924c9d">'∀'</span> 0104 0105 anotherString <span style="color:#006e28">:</span> String 0106 anotherString <span style="color:#006e28">=</span> <span style="color:#bf0303">"¬ be\</span> 0107 <span style="color:#bf0303"> \pa"</span> 0108 0109 nat <span style="color:#006e28">:</span> ℕ 0110 nat <span style="color:#006e28">=</span> <span style="color:#b08000">45</span> 0111 0112 float <span style="color:#006e28">:</span> Float 0113 float <span style="color:#006e28">=</span> <span style="color:#b08000">45.0e-37</span> 0114 0115 <span style="color:#898887">-- 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:#006e28">=</span> Test<span style="color:#006e28">.</span>Equiv <span style="color:#006e28">{</span>Test<span style="color:#006e28">.</span>ℕ<span style="color:#006e28">}</span> 0119 </pre></body></html>