# HG changeset patch
# User atton
# Date 1479407679 0
# Node ID bf26f11058626cf8b4b9cabd103b96ec1b1c4bde
# Parent  b0c6e0392b00d46c97a03625b60c1fae32ba3d81
Generalize lemma

diff -r b0c6e0392b00 -r bf26f1105862 src/parallel_execution/stack.agda
--- a/src/parallel_execution/stack.agda	Thu Nov 17 18:28:13 2016 +0000
+++ b/src/parallel_execution/stack.agda	Thu Nov 17 18:34:39 2016 +0000
@@ -77,10 +77,9 @@
 test02 : {a : Set} -> SingleLinkedStack a -> Bool
 test02 stack = (popSingleLinkedStack stack) test01
 
-test03 :  Bool
-test03 = pushSingleLinkedStack emptySingleLinkedStack (cons True Nothing) test02 -- ok
---test03 = pushSingleLinkedStack emptySingleLinkedStack (False) test02 -- ok
+test03 : {a : Set} -> a ->  Bool
+test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02
 
 
-lemma : test03 ≡ False
+lemma : {A : Set} {a : A} -> test03 a ≡ False
 lemma = refl