← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/simple-lib/Lib/Nat.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/simple-lib/Lib/Nat.agda
1
 
 
2
 
module Lib.Nat where
3
 
 
4
 
open import Lib.Bool
5
 
open import Lib.Logic
6
 
open import Lib.Id
7
 
 
8
 
data Nat : Set where
9
 
  zero : Nat
10
 
  suc  : Nat -> Nat
11
 
 
12
 
{-# BUILTIN NATURAL Nat  #-}
13
 
{-# BUILTIN ZERO    zero #-}
14
 
{-# BUILTIN SUC     suc  #-}
15
 
 
16
 
infixr 50 _*_
17
 
infixr 40 _+_
18
 
 
19
 
_+_ : Nat -> Nat -> Nat
20
 
zero  + m = m
21
 
suc n + m = suc (n + m)
22
 
 
23
 
lem-plus-zero : (n : Nat) -> n + 0 ≡ n
24
 
lem-plus-zero  zero   = refl
25
 
lem-plus-zero (suc n) = cong suc (lem-plus-zero n)
26
 
 
27
 
lem-plus-suc : (n m : Nat) -> n + suc m ≡ suc (n + m)
28
 
lem-plus-suc  zero   m = refl
29
 
lem-plus-suc (suc n) m = cong suc (lem-plus-suc n m)
30
 
 
31
 
lem-plus-commute : (n m : Nat) -> n + m ≡ m + n
32
 
lem-plus-commute n  zero   = lem-plus-zero _
33
 
lem-plus-commute n (suc m) with n + suc m | lem-plus-suc n m
34
 
... | .(suc (n + m)) | refl = cong suc (lem-plus-commute n m)
35
 
 
36
 
_*_ : Nat -> Nat -> Nat
37
 
zero  * m = zero
38
 
suc n * m = m + n * m
39
 
 
40
 
{-# BUILTIN NATPLUS  _+_ #-}
41
 
{-# BUILTIN NATTIMES _*_ #-}
42
 
 
43
 
_==_ : Nat -> Nat -> Bool
44
 
zero  == zero  = true
45
 
zero  == suc _ = false
46
 
suc _ == zero  = false
47
 
suc n == suc m = n == m
48
 
 
49
 
{-# BUILTIN NATEQUALS _==_ #-}
50
 
 
51
 
NonZero : Nat -> Set
52
 
NonZero zero    = False
53
 
NonZero (suc _) = True