# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1400655950 -32400
# Node ID f922e687f3a1869b9769b6f81abf6dc65c164900
# Parent  db4c6d435f23113f3aa1c06f6ddaa0b626395c0c
Define multiply

diff -r db4c6d435f23 -r f922e687f3a1 int.agda
--- 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