← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to examples/syntax/highlighting/Test.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

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