← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/AIM4/bag/Pos.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/AIM4/bag/Pos.agda
1
 
 
2
 
module Pos where
3
 
 
4
 
  import Prelude
5
 
  import Equiv
6
 
  import Datoid
7
 
  import Nat
8
 
 
9
 
  open Prelude
10
 
  open Equiv
11
 
  open Datoid
12
 
 
13
 
  abstract
14
 
 
15
 
    Pos : Set
16
 
    Pos = Nat.Nat
17
 
 
18
 
    one : Pos
19
 
    one = Nat.zero
20
 
 
21
 
    suc : Pos -> Pos
22
 
    suc = Nat.suc
23
 
 
24
 
    suc' : Nat.Nat -> Pos
25
 
    suc' n = n
26
 
 
27
 
    _+_ : Pos -> Pos -> Pos
28
 
    m + n = suc (Nat._+_ m n)
29
 
 
30
 
    -- Returns Nothing if input is 1.
31
 
    pred : Pos -> Maybe Pos
32
 
    pred Nat.zero    = Nothing
33
 
    pred (Nat.suc n) = Just n
34
 
 
35
 
    toNat : Pos -> Nat.Nat
36
 
    toNat = suc
37
 
 
38
 
    decidableEquiv : DecidableEquiv Pos
39
 
    decidableEquiv = Nat.decidableEquiv
40
 
 
41
 
  posDatoid : Datoid
42
 
  posDatoid = datoid Pos decidableEquiv
43
 
 
44
 
  sucPred : Maybe Pos -> Pos
45
 
  sucPred Nothing  = one
46
 
  sucPred (Just p) = suc p
47
 
 
48
 
  data Pred (p : Pos) (mP : Maybe Pos) : Set where
49
 
    ok : datoidRel posDatoid (sucPred mP) p -> Pred p mP
50
 
 
51
 
  abstract
52
 
 
53
 
    -- Returns Nothing if input is 1.
54
 
    predOK : (p : Pos) -> Pred p (pred p)
55
 
    predOK Nat.zero    = ok (dRefl posDatoid {one})
56
 
    predOK (Nat.suc n) = ok (dRefl posDatoid {n})