Mercurial > hg > Members > atton > agda > systemT
changeset 7:f922e687f3a1
Define multiply
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 21 May 2014 16:05:50 +0900 (2014-05-21) |
parents | db4c6d435f23 |
children | e191792472f8 |
files | int.agda |
diffstat | 1 files changed, 13 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/int.agda Wed May 21 14:55:52 2014 +0900 +++ b/int.agda Wed May 21 16:05:50 2014 +0900 @@ -4,6 +4,12 @@ module int where +double : Int -> Int +double O = O +double (S n) = S (S (double n)) + + +infixl 30 _+_ _+_ : Int -> Int -> Int n + O = n n + (S m) = S (n + m) @@ -12,10 +18,6 @@ left-increment n O = refl left-increment n (S m) = cong S (left-increment n m) -double : Int -> Int -double O = O -double (S n) = S (S (double n)) - sum-sym : (n : Int) (m : Int) -> n + m ≡ m + n sum-sym O O = refl sum-sym O (S m) = cong S (sum-sym O m) @@ -43,3 +45,10 @@ sum-assoc (S x) O (S z) = cong S (sum-assoc (S x) O z) sum-assoc (S x) (S y) O = refl sum-assoc (S x) (S y) (S z) = cong S (sum-assoc (S x) (S y) z) + + +infixl 40 _*_ +_*_ : Int -> Int -> Int +n * O = O +n * (S O) = n +n * (S m) = n + (n * m) \ No newline at end of file