changeset 7:f922e687f3a1

Define multiply
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 21 May 2014 16:05:50 +0900
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