Mercurial > hg > Members > Moririn

diff src/parallel_execution/stack.agda @ 165:bf26f1105862

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Generalize lemma
author atton
date Thu, 17 Nov 2016 18:34:39 +0000
parents b0c6e0392b00
children b3be97ba0782
line wrap: on
line diff
--- 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