--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/stack.agda	Tue Nov 15 19:02:36 2016 +0900
@@ -0,0 +1,16 @@
+module stack where
+
+pushSingleLinkedStack : Stack -> Data -> (Code : Stack -> ?) -> ?
+pushSingleLinkedStack stack data next = next stack1
+  where
+    element = record {next = top stack; data = data}
+    stack1  = record {top = just element}
+
+
+popSingleLinkedStack : Maybe ?? -> Data -> (Code : Stack -> (Maybe ??) -> ?) -> ?
+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)}