File indexing completed on 2025-02-02 03:54:47
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>