# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1514801821 -32400
# Node ID 0bec9490c199f10c2af709cf0f5e98b554da5982
# Parent  413ce51da50bcd3fb6ea1b59e911731806ed862b
stack.agda comment

diff -r 413ce51da50b -r 0bec9490c199 src/parallel_execution/stack.agda
--- a/src/parallel_execution/stack.agda	Mon Jan 01 19:14:09 2018 +0900
+++ b/src/parallel_execution/stack.agda	Mon Jan 01 19:17:01 2018 +0900
@@ -183,6 +183,8 @@
 -- this should be proved by properties of the stack inteface, not only by the implementation,
 --    and the implementation have to provides the properties.
 --
+--    we cannot write "s ≡ s3", since level of the Set does not fit , but we cant use stack s ≡ stack s3
+--  
 -- push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : Stack (SingleLinkedStack D) ) ->
 --     pushStack s x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> ((stack s ≡ stack s3 )  ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))))
 -- push->push->pop2 {l} {D} x y s = {!!}