Mercurial > hg > Members > atton > agda > systemT

comparison int.agda @ 7:f922e687f3a1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define multiply
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 21 May 2014 16:05:50 +0900
parents db4c6d435f23
children e191792472f8
comparison
equal deleted inserted replaced
6:db4c6d435f23 7:f922e687f3a1
2 open import Relation.Binary.PropositionalEquality 2 open import Relation.Binary.PropositionalEquality
3 open ≡-Reasoning 3 open ≡-Reasoning
4 4
5 module int where 5 module int where
6 6
7 double : Int -> Int
8 double O = O
9 double (S n) = S (S (double n))
10
11
12 infixl 30 _+_
7 _+_ : Int -> Int -> Int 13 _+_ : Int -> Int -> Int
8 n + O = n 14 n + O = n
9 n + (S m) = S (n + m) 15 n + (S m) = S (n + m)
10 16
11 left-increment : (n m : Int) -> (S n) + m ≡ S (n + m) 17 left-increment : (n m : Int) -> (S n) + m ≡ S (n + m)
12 left-increment n O = refl 18 left-increment n O = refl
13 left-increment n (S m) = cong S (left-increment n m) 19 left-increment n (S m) = cong S (left-increment n m)
14
15 double : Int -> Int
16 double O = O
17 double (S n) = S (S (double n))
18 20
19 sum-sym : (n : Int) (m : Int) -> n + m ≡ m + n 21 sum-sym : (n : Int) (m : Int) -> n + m ≡ m + n
20 sum-sym O O = refl 22 sum-sym O O = refl
21 sum-sym O (S m) = cong S (sum-sym O m) 23 sum-sym O (S m) = cong S (sum-sym O m)
22 sum-sym (S n) O = cong S (sum-sym n O) 24 sum-sym (S n) O = cong S (sum-sym n O)
41 sum-assoc O (S y) (S z) = cong S (sum-assoc O (S y) z) 43 sum-assoc O (S y) (S z) = cong S (sum-assoc O (S y) z)
42 sum-assoc (S x) O O = refl 44 sum-assoc (S x) O O = refl
43 sum-assoc (S x) O (S z) = cong S (sum-assoc (S x) O z) 45 sum-assoc (S x) O (S z) = cong S (sum-assoc (S x) O z)
44 sum-assoc (S x) (S y) O = refl 46 sum-assoc (S x) (S y) O = refl
45 sum-assoc (S x) (S y) (S z) = cong S (sum-assoc (S x) (S y) z) 47 sum-assoc (S x) (S y) (S z) = cong S (sum-assoc (S x) (S y) z)
48
49
50 infixl 40 _*_
51 _*_ : Int -> Int -> Int
52 n * O = O
53 n * (S O) = n
54 n * (S m) = n + (n * m)