Mercurial > hg > Gears > GearsAgda
changeset 504:0bec9490c199
stack.agda comment
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 01 Jan 2018 19:17:01 +0900 |
| parents | 413ce51da50b |
| children | 528c31b045de |
| files | src/parallel_execution/stack.agda |
| diffstat | 1 files changed, 2 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- 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 = {!!}