# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1462258914 -32400
# Node ID 14c22339ce06e37e10811c5f588b38c0ce79d106
# Parent  a59bebe0265a51224f3993ae493c992090770b98
Define state in agda

diff -r a59bebe0265a -r 14c22339ce06 state/state.agda
--- a/state/state.agda	Fri Dec 11 20:27:04 2015 +0900
+++ b/state/state.agda	Tue May 03 16:01:54 2016 +0900
@@ -15,28 +15,23 @@
 
 module state where
 
-record Product {l ll : Level} (A : Set l) (B : Set ll) : Set (suc (l ⊔ ll)) where 
+record Product {l : Level} (A B : Set l) : Set (suc l) where 
   constructor <_,_>
   field
     first  : A
     second : B
 open Product
 
-product-create : {l ll : Level} {A : Set l} {B : Set ll} -> A -> B -> Product A B
-product-create a b = < a , b >
-
-
-record State {l ll : Level} (S : Set l) (A : Set ll) : Set (suc (l ⊔ ll)) where
+record State {l : Level} (S A : Set l) : Set (suc l) where
   field
     runState : S -> Product A S
 open State
 
-state : {l ll : Level} {S : Set l} {A : Set ll} -> (S -> Product A S) -> State S A
+state : {l : Level} {S A : Set l} -> (S -> Product A S) -> State S A
 state f = record {runState = f}
 
-return : {l ll : Level} {S : Set l} {A : Set ll} -> A -> State S A
+return : {l : Level} {S A : Set l}  -> A -> State S A
 return a = state (\s -> < a , s > )
 
-
-_>>=_ : {l ll lll : Level} {S : Set l} {A : Set ll} {B : Set lll} -> State S A -> (A -> State S B) -> State S B
-m >>= k = {!!}
\ No newline at end of file
+_>>=_ : {l : Level} {S A B : Set l} -> State S A -> (A -> State S B) -> State S B
+m  >>= k =  state (\s -> (State.runState (k (Product.first (State.runState m s))) (Product.second (State.runState m s))))
\ No newline at end of file