Mercurial > hg > Papers > 2019 > oshiro-thesis
annotate final_pre/src/AgdaStackSomeState.agda.replaced @ 7:0e8b9646d43f
add final_pre
author | e155702 |
---|---|
date | Sun, 17 Feb 2019 05:39:59 +0900 |
parents | |
children |
rev | line source |
---|---|
7 | 1 stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) @$\rightarrow$@ Stack {l} {m} D {t} ( SingleLinkedStack D ) |
2 stackInSomeState s = record { stack = s ; stackMethods = singleLinkedStackSpec } | |
3 | |
4 push@$\rightarrow$@push@$\rightarrow$@pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) @$\rightarrow$@ pushStack (stackInSomeState s) x (\s1 @$\rightarrow$@ pushStack s1 y (\s2 @$\rightarrow$@ pop2Stack s2 (\s3 y1 x1 @$\rightarrow$@ | |
5 (Just x @$\equiv$@ x1) ∧ (Just y @$\equiv$@ y1)))) | |
6 push@$\rightarrow$@push@$\rightarrow$@pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl } |