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