--- a/src/parallel_execution/stack.agda	Thu Dec 28 15:02:23 2017 +0900
+++ b/src/parallel_execution/stack.agda	Thu Dec 28 15:52:01 2017 +0900
@@ -1,6 +1,7 @@
 module stack where
 
 open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
 
 data Nat : Set where
   zero : Nat
@@ -10,6 +11,12 @@
   True  : Bool
   False : Bool
 
+-- equal : {a : Set} -> a -> a -> Bool
+-- equal x y with (x ≡)y)
+-- equal x .x | refl = True
+-- equal _ _ | _ = False
+
+
 data Maybe (a : Set) : Set  where
   Nothing : Maybe a
   Just    : a -> Maybe a
@@ -20,11 +27,13 @@
     push : stackImpl -> a -> (stackImpl -> t) -> t
     pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
 
-pushStack : {a t : Set} -> Stack -> a -> (Stack -> t) -> t
-pushStack {a} {t} s0 d next = (stackImpl s0) (stack s0) d (\s1 -> next (record s0 {stack = s1;} ))
+open Stack
 
-popStack : {a t : Set} -> Stack -> (Stack -> t) -> t
-popStack {a} {t} s0  next = (stackImpl s0) (stack s0) (\s1 -> next s0)
+pushStack : {a t si : Set} -> Stack si -> a -> (Stack si -> t) -> t
+pushStack {a} {t} s0 d next = push s0 (stack s0) d (\s1 -> next (record s0 {stack = s1} ))
+
+popStack : {a t si : Set} -> Stack si -> (Stack si -> Maybe a  -> t) -> t
+popStack {a} {t} s0  next = pop s0 (stack s0) (\s1 d1 -> next (record s0 {stack = s1}) d1 )
 
 
 data Element (a : Set) : Set where
@@ -91,6 +100,11 @@
 test03 : {a : Set} -> a ->  Bool
 test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02
 
+testStack01 : {a : Set} -> a -> Bool
+testStack01 v = pushStack createSingleLinkedStack v (
+   \s -> popStack s (\s1 d1 -> True))
+
+
 
 lemma : {A : Set} {a : A} -> test03 a ≡ False
 lemma = refl