autotests/folding/test.agda.fold

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.ℕ}