Mercurial > hg > Gears > GearsAgda

changeset 502:8d997f0c9b2c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
stack.agda comment
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 01 Jan 2018 18:58:05 +0900
parents 55077dd40a51
children 413ce51da50b
files src/parallel_execution/stack.agda
diffstat 1 files changed, 10 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/stack.agda	Mon Jan 01 18:32:20 2018 +0900
+++ b/src/parallel_execution/stack.agda	Mon Jan 01 18:58:05 2018 +0900
@@ -177,8 +177,17 @@
 
 ------
 -- 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 ) ) ))))
+--     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 = {!!}
+--    where
+--       t0 :  (s3 : Stack {_} {succ l} {D} {Set l} (SingleLinkedStack D)) (x1 y1 : Maybe D) -> (stack s ≡ stack s3 )  ->  (Just x ≡ x1 ) -> (Just y ≡ y1 )
+--           -> ((stack s ≡ stack s3 )  ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) )) 
+--       t0 s3 x1 y1 refl refl refl = record { pi1 = refl ; pi2 = record { pi1 = refl ; pi2 = refl } }
+--       t1 :  (s2 : Stack (SingleLinkedStack D))  ->   pop2Stack s2 ( \s3 y1 x1 -> ((stack s ≡ stack s3 )  ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+--       t1 s2 = {!!} 
+--       t2 :  (s1 : Stack (SingleLinkedStack D)) (x1 y1 : Maybe D) ->   
+--            pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> ((stack s ≡ stack s3 )  ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ) ))
+--       t2 s1 = {!!}
 
 
 id : {n : Level} {A : Set n} -> A -> A