# HG changeset patch
# User atton
# Date 1479208651 -32400
# Node ID 0aa2265660a01cc4cb6be964da4f2a4ef2260d8e
# Parent  19cc626943e41ddde504c3dfd30033dea440be0f
Add stack lemma

diff -r 19cc626943e4 -r 0aa2265660a0 src/parallel_execution/stack.agda
--- a/src/parallel_execution/stack.agda	Tue Nov 15 19:33:13 2016 +0900
+++ b/src/parallel_execution/stack.agda	Tue Nov 15 20:17:31 2016 +0900
@@ -28,10 +28,24 @@
     stack1  = record {top = just element}
 
 
-popSingleLinkedStack : {a : Set} -> Maybe a -> Data -> (Code : Stack -> (Maybe a) -> T) -> T
+popSingleLinkedStack : {a : Set} -> Maybe a -> (Code : Stack -> (Maybe a) -> T) -> T
 popSingleLinkedStack stack data next with (top stack) =
   ... | nothing = next stack nothing
   ... | just a  = next stack1 data1
     where
       data1 = data a
       stack1 = record { top = (next a)}
+
+
+test01 : Stack -> Maybe a -> T
+test01 stack nothing  = false
+test01 stack (just _) = true
+
+test02 : Stack -> T
+test02 stack = (pop stack) test01
+
+test03 : T
+test03 = push createSingleLinkedStack true test02
+
+lemma : test01 == false
+lemma = refl
\ No newline at end of file