← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/AIM6/HelloAgda/Records.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/AIM6/HelloAgda/Records.agda
1
 
{-
2
 
 
3
 
        Agda Implementors' Meeting VI
4
 
 
5
 
                  Göteborg
6
 
             May 24 - 30, 2007
7
 
 
8
 
 
9
 
                Hello Agda!
10
 
 
11
 
                Ulf Norell
12
 
 
13
 
-}
14
 
 
15
 
 
16
 
module Records where
17
 
 
18
 
open import Naturals
19
 
open import Bool
20
 
 
21
 
{-
22
 
 
23
 
  A very simple record.
24
 
 
25
 
-}
26
 
 
27
 
record Point : Set where
28
 
  field x : Nat
29
 
        y : Nat
30
 
 
31
 
data Point' : Set where
32
 
  mkPoint : (x : Nat)(y : Nat) -> Point'
33
 
 
34
 
 
35
 
origin : Point
36
 
origin = record { x = 0; y = 0 }
37
 
 
38
 
origin' : Point'
39
 
origin' = mkPoint 0 0
40
 
 
41
 
{-
42
 
  module Point (p : Point) where
43
 
    x : Nat
44
 
    y : Nat
45
 
-}
46
 
 
47
 
getX : Point -> Nat
48
 
getX = Point.x
49
 
 
50
 
sum : Point -> Nat
51
 
sum p = x + y
52
 
  where
53
 
   open module Pp = Point p
54
 
 
55
 
 
56
 
data _==_ {A : Set}(x : A) : A -> Set where
57
 
  refl : x == x
58
 
 
59
 
η-Point : (p : Point) -> p == record { x = Point.x p; y = Point.y p }
60
 
η-Point p = refl
61
 
 
62
 
{-
63
 
 
64
 
  The empty record
65
 
 
66
 
-}
67
 
 
68
 
record True : Set where
69
 
 
70
 
tt : True
71
 
tt = record{}
72
 
 
73
 
 
74
 
data False : Set where
75
 
 
76
 
NonZero : Nat -> Set
77
 
NonZero zero    = False
78
 
NonZero (suc _) = True
79
 
 
80
 
 
81
 
_/_ : (n m : Nat){p : NonZero m} -> Nat
82
 
(n / zero) {}
83
 
zero  / suc m = zero
84
 
suc n / suc m = div (suc n) (suc m) m
85
 
  where
86
 
    div : Nat -> Nat -> Nat -> Nat
87
 
    div  zero    zero   c = suc zero
88
 
    div  zero   (suc y) c = zero
89
 
    div (suc x)  zero   c = suc (div x c c)
90
 
    div (suc x) (suc y) c = div x y c
91
 
 
92
 
 
93
 
five = 17 / 3
94
 
 
95
 
{-
96
 
 
97
 
  A dependent record
98
 
 
99
 
-}
100
 
 
101
 
record ∃ {A : Set}(P : A -> Set) : Set where
102
 
  field
103
 
    witness : A
104
 
    proof   : P witness