← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/SummerSchool07/Lecture/Datatypes.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/SummerSchool07/Lecture/Datatypes.agda
1
 
{-
2
 
 
3
 
          Types Summer School 2007
4
 
 
5
 
                 Bertinoro
6
 
             Aug 19 - 31, 2007
7
 
 
8
 
 
9
 
                   Agda
10
 
 
11
 
                Ulf Norell
12
 
 
13
 
-}
14
 
 
15
 
 
16
 
module Datatypes where
17
 
 
18
 
{-
19
 
 
20
 
  Simple datatypes.
21
 
 
22
 
-}
23
 
 
24
 
 
25
 
data Nat : Set where
26
 
  zero : Nat
27
 
  suc  : Nat -> Nat
28
 
 
29
 
pred : Nat -> Nat
30
 
pred zero    = zero
31
 
pred (suc n) = n
32
 
 
33
 
_+_ : Nat -> Nat -> Nat
34
 
zero  + m = m
35
 
suc n + m = suc (n + m)
36
 
 
37
 
infixl 60 _+_
38
 
 
39
 
 
40
 
data Bool : Set where
41
 
  true  : Bool
42
 
  false : Bool
43
 
 
44
 
if_then_else_ : {A : Set} -> Bool -> A -> A -> A
45
 
if true  then x else y = x
46
 
if_then_else_ false x y = y
47
 
 
48
 
{-
49
 
 
50
 
  Parameterised datatypes
51
 
 
52
 
-}
53
 
 
54
 
data List (A : Set) : Set where
55
 
  []   : List A
56
 
  _::_ : A -> List A -> List A
57
 
 
58
 
nil : (A : Set) -> List A
59
 
nil A = [] {A}
60
 
 
61
 
map : {A B : Set} -> (A -> B) -> List A -> List B
62
 
map f []        = []
63
 
map f (x :: xs) = f x :: map f xs
64
 
 
65
 
{-
66
 
 
67
 
  Empty datatypes
68
 
 
69
 
-}
70
 
 
71
 
data False : Set where
72
 
 
73
 
 
74
 
elim-False : {A : Set} -> False -> A
75
 
elim-False ()  -- Look Ma, no right hand side!
76
 
 
77
 
 
78
 
{-
79
 
 
80
 
  What's next?
81
 
 
82
 
-}
83