1-- Agda Sample File 2-- https://github.com/agda/agda/blob/master/examples/syntax/highlighting/Test.agda 3 4-- This test file currently lacks module-related stuff. 5 6{- Nested 7 {- comment. -} -} 8 9module Test where 10 11infix 12 _! 12infixl 7 _+_ _-_ 13infixr 2 -_ 14 15postulate x : Set 16 17f : (Set -> Set -> Set) -> Set 18f _*_ = x * x 19 20data ℕ : Set where 21 zero : ℕ 22 suc : ℕ -> ℕ 23 24_+_ : ℕ -> ℕ -> ℕ 25zero + n = n 26suc m + n = suc (m + n) 27 28postulate _-_ : ℕ -> ℕ -> ℕ 29 30-_ : ℕ -> ℕ 31- n = n 32 33_! : ℕ -> ℕ 34zero ! = suc zero 35suc n ! = n - n ! 36 37record Equiv {a : Set} (_≈_ : a -> a -> Set) : Set where 38 field 39 refl : forall x -> x ≈ x 40 sym : {x y : a} -> x ≈ y -> y ≈ x 41 _`trans`_ : forall {x y z} -> x ≈ y -> y ≈ z -> x ≈ z 42 43data _≡_ {a : Set} (x : a) : a -> Set where 44 refl : x ≡ x 45 46subst : forall {a x y} -> 47 (P : a -> Set) -> x ≡ y -> P x -> P y 48subst {x = x} .{y = x} _ refl p = p 49 50Equiv-≡ : forall {a} -> Equiv {a} _≡_ 51Equiv-≡ {a} = 52 record { refl = \_ -> refl 53 ; sym = sym 54 ; _`trans`_ = _`trans`_ 55 } 56 where 57 sym : {x y : a} -> x ≡ y -> y ≡ x 58 sym refl = refl 59 60 _`trans`_ : {x y z : a} -> x ≡ y -> y ≡ z -> x ≡ z 61 refl `trans` refl = refl 62 63postulate 64 String : Set 65 Char : Set 66 Float : Set 67 68data Int : Set where 69 pos : ℕ → Int 70 negsuc : ℕ → Int 71 72{-# BUILTIN STRING String #-} 73{-# BUILTIN CHAR Char #-} 74{-# BUILTIN FLOAT Float #-} 75 76{-# BUILTIN NATURAL ℕ #-} 77 78{-# BUILTIN INTEGER Int #-} 79{-# BUILTIN INTEGERPOS pos #-} 80{-# BUILTIN INTEGERNEGSUC negsuc #-} 81 82data [_] (a : Set) : Set where 83 [] : [ a ] 84 _∷_ : a -> [ a ] -> [ a ] 85 86{-# BUILTIN LIST [_] #-} 87{-# BUILTIN NIL [] #-} 88{-# BUILTIN CONS _∷_ #-} 89 90primitive 91 primStringToList : String -> [ Char ] 92 93string : [ Char ] 94string = primStringToList "∃ apa" 95 96char : Char 97char = '∀' 98 99anotherString : String 100anotherString = "¬ be\ 101 \pa" 102 103nat : ℕ 104nat = 45 105 106float : Float 107float = 45.0e-37 108 109-- Testing qualified names. 110 111open import Test 112Eq = Test.Equiv {Test.ℕ} 113