Warning, /frameworks/syntax-highlighting/autotests/reference/test.agda.ref is written in an unsupported language. File is not indexed.
0001 <Comment>-- Agda Sample File</Comment><br/>
0002 <Comment>-- https://github.com/agda/agda/blob/master/examples/syntax/highlighting/Test.agda</Comment><br/>
0003 <Normal></Normal><br/>
0004 <Comment>-- This test file currently lacks module-related stuff.</Comment><br/>
0005 <Normal></Normal><br/>
0006 <Comment>{- Nested</Comment><br/>
0007 <Comment> {- comment. -} -}</Comment><br/>
0008 <Normal></Normal><br/>
0009 <Keyword>module</Keyword><Normal> Test </Normal><Keyword>where</Keyword><br/>
0010 <Normal></Normal><br/>
0011 <Keyword>infix</Keyword><Normal> </Normal><Decimal>12</Decimal><Normal> </Normal><Special>_</Special><Normal>!</Normal><br/>
0012 <Keyword>infixl</Keyword><Normal> </Normal><Decimal>7</Decimal><Normal> </Normal><Special>_</Special><Normal>+</Normal><Special>_</Special><Normal> </Normal><Special>_</Special><Normal>-</Normal><Special>_</Special><br/>
0013 <Keyword>infixr</Keyword><Normal> </Normal><Decimal>2</Decimal><Normal> -</Normal><Special>_</Special><br/>
0014 <Normal></Normal><br/>
0015 <Keyword>postulate</Keyword><Normal> x </Normal><Special>:</Special><Normal> </Normal><Type>Set</Type><br/>
0016 <Normal></Normal><br/>
0017 <Normal>f </Normal><Special>:</Special><Normal> </Normal><Special>(</Special><Type>Set</Type><Normal> </Normal><Special>-></Special><Normal> </Normal><Type>Set</Type><Normal> </Normal><Special>-></Special><Normal> </Normal><Type>Set</Type><Special>)</Special><Normal> </Normal><Special>-></Special><Normal> </Normal><Type>Set</Type><br/>
0018 <Normal>f </Normal><Special>_</Special><Normal>*</Normal><Special>_</Special><Normal> </Normal><Special>=</Special><Normal> x * x</Normal><br/>
0019 <Normal></Normal><br/>
0020 <Keyword>data</Keyword><Normal> ℕ </Normal><Special>:</Special><Normal> </Normal><Type>Set</Type><Normal> </Normal><Keyword>where</Keyword><br/>
0021 <Normal> zero </Normal><Special>:</Special><Normal> ℕ</Normal><br/>
0022 <Normal> suc </Normal><Special>:</Special><Normal> ℕ </Normal><Special>-></Special><Normal> ℕ</Normal><br/>
0023 <Normal></Normal><br/>
0024 <Special>_</Special><Normal>+</Normal><Special>_</Special><Normal> </Normal><Special>:</Special><Normal> ℕ </Normal><Special>-></Special><Normal> ℕ </Normal><Special>-></Special><Normal> ℕ</Normal><br/>
0025 <Normal>zero + n </Normal><Special>=</Special><Normal> n</Normal><br/>
0026 <Normal>suc m + n </Normal><Special>=</Special><Normal> suc </Normal><Special>(</Special><Normal>m + n</Normal><Special>)</Special><br/>
0027 <Normal></Normal><br/>
0028 <Keyword>postulate</Keyword><Normal> </Normal><Special>_</Special><Normal>-</Normal><Special>_</Special><Normal> </Normal><Special>:</Special><Normal> ℕ </Normal><Special>-></Special><Normal> ℕ </Normal><Special>-></Special><Normal> ℕ</Normal><br/>
0029 <Normal></Normal><br/>
0030 <Normal>-</Normal><Special>_</Special><Normal> </Normal><Special>:</Special><Normal> ℕ </Normal><Special>-></Special><Normal> ℕ</Normal><br/>
0031 <Normal>- n </Normal><Special>=</Special><Normal> n</Normal><br/>
0032 <Normal></Normal><br/>
0033 <Special>_</Special><Normal>! </Normal><Special>:</Special><Normal> ℕ </Normal><Special>-></Special><Normal> ℕ</Normal><br/>
0034 <Normal>zero ! </Normal><Special>=</Special><Normal> suc zero</Normal><br/>
0035 <Normal>suc n ! </Normal><Special>=</Special><Normal> n - n !</Normal><br/>
0036 <Normal></Normal><br/>
0037 <Keyword>record</Keyword><Normal> Equiv </Normal><Special>{</Special><Normal>a </Normal><Special>:</Special><Normal> </Normal><Type>Set</Type><Special>}</Special><Normal> </Normal><Special>(_</Special><Normal>≈</Normal><Special>_</Special><Normal> </Normal><Special>:</Special><Normal> a </Normal><Special>-></Special><Normal> a </Normal><Special>-></Special><Normal> </Normal><Type>Set</Type><Special>)</Special><Normal> </Normal><Special>:</Special><Normal> </Normal><Type>Set</Type><Normal> </Normal><Keyword>where</Keyword><br/>
0038 <Normal> </Normal><Keyword>field</Keyword><br/>
0039 <Normal> refl </Normal><Special>:</Special><Normal> </Normal><Keyword>forall</Keyword><Normal> x </Normal><Special>-></Special><Normal> x ≈ x</Normal><br/>
0040 <Normal> sym </Normal><Special>:</Special><Normal> </Normal><Special>{</Special><Normal>x y </Normal><Special>:</Special><Normal> a</Normal><Special>}</Special><Normal> </Normal><Special>-></Special><Normal> x ≈ y </Normal><Special>-></Special><Normal> y ≈ x</Normal><br/>
0041 <Normal> </Normal><Special>_</Special><Normal>`trans`</Normal><Special>_</Special><Normal> </Normal><Special>:</Special><Normal> </Normal><Keyword>forall</Keyword><Normal> </Normal><Special>{</Special><Normal>x y z</Normal><Special>}</Special><Normal> </Normal><Special>-></Special><Normal> x ≈ y </Normal><Special>-></Special><Normal> y ≈ z </Normal><Special>-></Special><Normal> x ≈ z</Normal><br/>
0042 <Normal></Normal><br/>
0043 <Keyword>data</Keyword><Normal> </Normal><Special>_</Special><Normal>≡</Normal><Special>_</Special><Normal> </Normal><Special>{</Special><Normal>a </Normal><Special>:</Special><Normal> </Normal><Type>Set</Type><Special>}</Special><Normal> </Normal><Special>(</Special><Normal>x </Normal><Special>:</Special><Normal> a</Normal><Special>)</Special><Normal> </Normal><Special>:</Special><Normal> a </Normal><Special>-></Special><Normal> </Normal><Type>Set</Type><Normal> </Normal><Keyword>where</Keyword><br/>
0044 <Normal> refl </Normal><Special>:</Special><Normal> x ≡ x</Normal><br/>
0045 <Normal></Normal><br/>
0046 <Normal>subst </Normal><Special>:</Special><Normal> </Normal><Keyword>forall</Keyword><Normal> </Normal><Special>{</Special><Normal>a x y</Normal><Special>}</Special><Normal> </Normal><Special>-></Special><br/>
0047 <Normal> </Normal><Special>(</Special><Normal>P </Normal><Special>:</Special><Normal> a </Normal><Special>-></Special><Normal> </Normal><Type>Set</Type><Special>)</Special><Normal> </Normal><Special>-></Special><Normal> x ≡ y </Normal><Special>-></Special><Normal> P x </Normal><Special>-></Special><Normal> P y</Normal><br/>
0048 <Normal>subst </Normal><Special>{</Special><Normal>x </Normal><Special>=</Special><Normal> x</Normal><Special>}</Special><Normal> </Normal><Special>.{</Special><Normal>y </Normal><Special>=</Special><Normal> x</Normal><Special>}</Special><Normal> </Normal><Special>_</Special><Normal> refl p </Normal><Special>=</Special><Normal> p</Normal><br/>
0049 <Normal></Normal><br/>
0050 <Normal>Equiv-≡ </Normal><Special>:</Special><Normal> </Normal><Keyword>forall</Keyword><Normal> </Normal><Special>{</Special><Normal>a</Normal><Special>}</Special><Normal> </Normal><Special>-></Special><Normal> Equiv </Normal><Special>{</Special><Normal>a</Normal><Special>}</Special><Normal> </Normal><Special>_</Special><Normal>≡</Normal><Special>_</Special><br/>
0051 <Normal>Equiv-≡ </Normal><Special>{</Special><Normal>a</Normal><Special>}</Special><Normal> </Normal><Special>=</Special><br/>
0052 <Normal> </Normal><Keyword>record</Keyword><Normal> </Normal><Special>{</Special><Normal> refl </Normal><Special>=</Special><Normal> </Normal><Special>\_</Special><Normal> </Normal><Special>-></Special><Normal> refl</Normal><br/>
0053 <Normal> </Normal><Special>;</Special><Normal> sym </Normal><Special>=</Special><Normal> sym</Normal><br/>
0054 <Normal> </Normal><Special>;</Special><Normal> </Normal><Special>_</Special><Normal>`trans`</Normal><Special>_</Special><Normal> </Normal><Special>=</Special><Normal> </Normal><Special>_</Special><Normal>`trans`</Normal><Special>_</Special><br/>
0055 <Normal> </Normal><Special>}</Special><br/>
0056 <Normal> </Normal><Keyword>where</Keyword><br/>
0057 <Normal> sym </Normal><Special>:</Special><Normal> </Normal><Special>{</Special><Normal>x y </Normal><Special>:</Special><Normal> a</Normal><Special>}</Special><Normal> </Normal><Special>-></Special><Normal> x ≡ y </Normal><Special>-></Special><Normal> y ≡ x</Normal><br/>
0058 <Normal> sym refl </Normal><Special>=</Special><Normal> refl</Normal><br/>
0059 <Normal></Normal><br/>
0060 <Normal> </Normal><Special>_</Special><Normal>`trans`</Normal><Special>_</Special><Normal> </Normal><Special>:</Special><Normal> </Normal><Special>{</Special><Normal>x y z </Normal><Special>:</Special><Normal> a</Normal><Special>}</Special><Normal> </Normal><Special>-></Special><Normal> x ≡ y </Normal><Special>-></Special><Normal> y ≡ z </Normal><Special>-></Special><Normal> x ≡ z</Normal><br/>
0061 <Normal> refl `trans` refl </Normal><Special>=</Special><Normal> refl</Normal><br/>
0062 <Normal></Normal><br/>
0063 <Keyword>postulate</Keyword><br/>
0064 <Normal> String </Normal><Special>:</Special><Normal> </Normal><Type>Set</Type><br/>
0065 <Normal> Char </Normal><Special>:</Special><Normal> </Normal><Type>Set</Type><br/>
0066 <Normal> Float </Normal><Special>:</Special><Normal> </Normal><Type>Set</Type><br/>
0067 <Normal></Normal><br/>
0068 <Keyword>data</Keyword><Normal> Int </Normal><Special>:</Special><Normal> </Normal><Type>Set</Type><Normal> </Normal><Keyword>where</Keyword><br/>
0069 <Normal> pos </Normal><Special>:</Special><Normal> ℕ </Normal><Special>→</Special><Normal> Int</Normal><br/>
0070 <Normal> negsuc </Normal><Special>:</Special><Normal> ℕ </Normal><Special>→</Special><Normal> Int</Normal><br/>
0071 <Normal></Normal><br/>
0072 <Pragma>{-# BUILTIN STRING String #-}</Pragma><br/>
0073 <Pragma>{-# BUILTIN CHAR Char #-}</Pragma><br/>
0074 <Pragma>{-# BUILTIN FLOAT Float #-}</Pragma><br/>
0075 <Normal></Normal><br/>
0076 <Pragma>{-# BUILTIN NATURAL ℕ #-}</Pragma><br/>
0077 <Normal></Normal><br/>
0078 <Pragma>{-# BUILTIN INTEGER Int #-}</Pragma><br/>
0079 <Pragma>{-# BUILTIN INTEGERPOS pos #-}</Pragma><br/>
0080 <Pragma>{-# BUILTIN INTEGERNEGSUC negsuc #-}</Pragma><br/>
0081 <Normal></Normal><br/>
0082 <Keyword>data</Keyword><Normal> [</Normal><Special>_</Special><Normal>] </Normal><Special>(</Special><Normal>a </Normal><Special>:</Special><Normal> </Normal><Type>Set</Type><Special>)</Special><Normal> </Normal><Special>:</Special><Normal> </Normal><Type>Set</Type><Normal> </Normal><Keyword>where</Keyword><br/>
0083 <Normal> [] </Normal><Special>:</Special><Normal> [ a ]</Normal><br/>
0084 <Normal> </Normal><Special>_</Special><Normal>∷</Normal><Special>_</Special><Normal> </Normal><Special>:</Special><Normal> a </Normal><Special>-></Special><Normal> [ a ] </Normal><Special>-></Special><Normal> [ a ]</Normal><br/>
0085 <Normal></Normal><br/>
0086 <Pragma>{-# BUILTIN LIST [_] #-}</Pragma><br/>
0087 <Pragma>{-# BUILTIN NIL [] #-}</Pragma><br/>
0088 <Pragma>{-# BUILTIN CONS _∷_ #-}</Pragma><br/>
0089 <Normal></Normal><br/>
0090 <Keyword>primitive</Keyword><br/>
0091 <Normal> primStringToList </Normal><Special>:</Special><Normal> String </Normal><Special>-></Special><Normal> [ Char ]</Normal><br/>
0092 <Normal></Normal><br/>
0093 <Normal>string </Normal><Special>:</Special><Normal> [ Char ]</Normal><br/>
0094 <Normal>string </Normal><Special>=</Special><Normal> primStringToList </Normal><String>"∃ apa"</String><br/>
0095 <Normal></Normal><br/>
0096 <Normal>char </Normal><Special>:</Special><Normal> Char</Normal><br/>
0097 <Normal>char </Normal><Special>=</Special><Normal> </Normal><Char>'∀'</Char><br/>
0098 <Normal></Normal><br/>
0099 <Normal>anotherString </Normal><Special>:</Special><Normal> String</Normal><br/>
0100 <Normal>anotherString </Normal><Special>=</Special><Normal> </Normal><String>"¬ be\</String><br/>
0101 <String> \pa"</String><br/>
0102 <Normal></Normal><br/>
0103 <Normal>nat </Normal><Special>:</Special><Normal> ℕ</Normal><br/>
0104 <Normal>nat </Normal><Special>=</Special><Normal> </Normal><Decimal>45</Decimal><br/>
0105 <Normal></Normal><br/>
0106 <Normal>float </Normal><Special>:</Special><Normal> Float</Normal><br/>
0107 <Normal>float </Normal><Special>=</Special><Normal> </Normal><Float>45.0e-37</Float><br/>
0108 <Normal></Normal><br/>
0109 <Comment>-- Testing qualified names.</Comment><br/>
0110 <Normal></Normal><br/>
0111 <Keyword>open</Keyword><Normal> </Normal><Keyword>import</Keyword><Normal> Test</Normal><br/>
0112 <Normal>Eq </Normal><Special>=</Special><Normal> Test</Normal><Special>.</Special><Normal>Equiv </Normal><Special>{</Special><Normal>Test</Normal><Special>.</Special><Normal>ℕ</Normal><Special>}</Special><br/>