Mercurial > hg > GearsTemplate

changeset 156:0aa2265660a0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add stack lemma
author atton
date Tue, 15 Nov 2016 20:17:31 +0900
parents 19cc626943e4
children 7cd629c29050
files src/parallel_execution/stack.agda
diffstat 1 files changed, 15 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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