Mercurial > hg > Members > Moririn

annotate stack.agda @ 574:70b09cbefd45

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add queue.agda
author ryokka
date Thu, 16 Aug 2018 18:22:08 +0900
parents 988c12d7f887
children 73fc32092b64
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
1 open import Level renaming (suc to succ ; zero to Zero )
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
2 module stack where
154
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
3
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
4 open import Relation.Binary.PropositionalEquality
477
c3202635c20a fix Stack.agda
ryokka
parents: 427
diff changeset
5 open import Relation.Binary.Core
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
6 open import Data.Nat
478
0223c07c3946 fix stack.agda
ryokka
parents: 477
diff changeset
7
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
8 ex : 1 + 2 ≡ 3
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
9 ex = refl
179
b3be97ba0782 Prove n-push/n-pop
atton
parents: 165
diff changeset
10
501
55077dd40a51 stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
11 data Bool {n : Level } : Set n where
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
12 True : Bool
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
13 False : Bool
164
b0c6e0392b00 Add comment to stack.agda
atton
parents: 161
diff changeset
14
501
55077dd40a51 stack.agda comment
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 500
diff changeset
15 record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
485
a7548f01f013 proof pop2 function in agda
ryokka
parents: 484
diff changeset
16 field
a7548f01f013 proof pop2 function in agda
ryokka
parents: 484
diff changeset
17 pi1 : a
a7548f01f013 proof pop2 function in agda
ryokka
parents: 484
diff changeset
18 pi2 : b
477
c3202635c20a fix Stack.agda
ryokka
parents: 427
diff changeset
19
554
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 544
diff changeset
20 data _∨_ {n : Level } (a : Set n) (b : Set n): Set n where
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 544
diff changeset
21 pi1 : a -> a ∨ b
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 544
diff changeset
22 pi2 : b -> a ∨ b
988c12d7f887 use another nat comparator
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 544
diff changeset
23
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
24 data Maybe {n : Level } (a : Set n) : Set n where
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
25 Nothing : Maybe a
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
26 Just : a -> Maybe a
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
27
574
70b09cbefd45 add queue.agda
ryokka
parents: 554
diff changeset
28 record StackMethods {n m : Level } (a : Set n ) {t : Set m } (stackImpl : Set n ) : Set (m Level.⊔ n) where
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
29 field
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
30 push : stackImpl -> a -> (stackImpl -> t) -> t
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
31 pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
32 pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
483
9098ec0a9e6b add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents: 478
diff changeset
33 get : stackImpl -> (stackImpl -> Maybe a -> t) -> t
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
34 get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
531
f6060e1bf900 add clearStack
ryokka
parents: 523
diff changeset
35 clear : stackImpl -> (stackImpl -> t) -> t
503
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
36 open StackMethods
427
07ccd411ad70 fix interface in agda
ryokka
parents: 181
diff changeset
37
515
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 511
diff changeset
38 record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
503
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
39 field
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
40 stack : si
515
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 511
diff changeset
41 stackMethods : StackMethods {n} {m} a {t} si
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 511
diff changeset
42 pushStack : a -> (Stack a si -> t) -> t
503
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
43 pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
515
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 511
diff changeset
44 popStack : (Stack a si -> Maybe a -> t) -> t
503
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
45 popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
515
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 511
diff changeset
46 pop2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t
503
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
47 pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
515
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 511
diff changeset
48 getStack : (Stack a si -> Maybe a -> t) -> t
503
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
49 getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
515
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 511
diff changeset
50 get2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t
503
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
51 get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
531
f6060e1bf900 add clearStack
ryokka
parents: 523
diff changeset
52 clearStack : (Stack a si -> t) -> t
f6060e1bf900 add clearStack
ryokka
parents: 523
diff changeset
53 clearStack next = clear (stackMethods ) (stack ) (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
54
503
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
55 open Stack
427
07ccd411ad70 fix interface in agda
ryokka
parents: 181
diff changeset
56
544
4f692df9b3db add reference
ryokka
parents: 537
diff changeset
57 {--
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
58 data Element {n : Level } (a : Set n) : Set n where
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
59 cons : a -> Maybe (Element a) -> Element a
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
60
544
4f692df9b3db add reference
ryokka
parents: 537
diff changeset
61
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
62 datum : {n : Level } {a : Set n} -> Element a -> a
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
63 datum (cons a _) = a
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
64
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
65 next : {n : Level } {a : Set n} -> Element a -> Maybe (Element a)
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
66 next (cons _ n) = n
544
4f692df9b3db add reference
ryokka
parents: 537
diff changeset
67 --}
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
68
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
69
164
b0c6e0392b00 Add comment to stack.agda
atton
parents: 161
diff changeset
70 -- cannot define recrusive record definition. so use linked list with maybe.
544
4f692df9b3db add reference
ryokka
parents: 537
diff changeset
71 record Element {l : Level} (a : Set l) : Set l where
4f692df9b3db add reference
ryokka
parents: 537
diff changeset
72 inductive
4f692df9b3db add reference
ryokka
parents: 537
diff changeset
73 constructor cons
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
74 field
164
b0c6e0392b00 Add comment to stack.agda
atton
parents: 161
diff changeset
75 datum : a -- `data` is reserved by Agda.
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
76 next : Maybe (Element a)
155
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
77
544
4f692df9b3db add reference
ryokka
parents: 537
diff changeset
78 open Element
155
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
79
164
b0c6e0392b00 Add comment to stack.agda
atton
parents: 161
diff changeset
80
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
81 record SingleLinkedStack {n : Level } (a : Set n) : Set n where
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
82 field
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
83 top : Maybe (Element a)
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
84 open SingleLinkedStack
155
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
85
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
86 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
87 pushSingleLinkedStack stack datum next = next stack1
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
88 where
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
89 element = cons datum (top stack)
164
b0c6e0392b00 Add comment to stack.agda
atton
parents: 161
diff changeset
90 stack1 = record {top = Just element}
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
91
155
19cc626943e4 stack.agda
atton
parents: 154
diff changeset
92
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
93 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
94 popSingleLinkedStack stack cs with (top stack)
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
95 ... | Nothing = cs stack Nothing
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
96 ... | Just d = cs stack1 (Just data1)
154
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
97 where
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
98 data1 = datum d
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
99 stack1 = record { top = (next d) }
154
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
100
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
101 pop2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
102 pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
103 ... | Nothing = cs stack Nothing Nothing
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
104 ... | Just d = pop2SingleLinkedStack' {n} {m} stack cs
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
105 where
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
106 pop2SingleLinkedStack' : {n m : Level } {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
107 pop2SingleLinkedStack' stack cs with (next d)
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
108 ... | Nothing = cs stack Nothing Nothing
511
044c25475ed4 fix stack.agda
mir3636
parents: 509
diff changeset
109 ... | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
110
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
111
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
112 getSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
483
9098ec0a9e6b add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents: 478
diff changeset
113 getSingleLinkedStack stack cs with (top stack)
9098ec0a9e6b add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents: 478
diff changeset
114 ... | Nothing = cs stack Nothing
9098ec0a9e6b add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents: 478
diff changeset
115 ... | Just d = cs stack (Just data1)
9098ec0a9e6b add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents: 478
diff changeset
116 where
9098ec0a9e6b add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents: 478
diff changeset
117 data1 = datum d
9098ec0a9e6b add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents: 478
diff changeset
118
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
119 get2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
120 get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
483
9098ec0a9e6b add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents: 478
diff changeset
121 ... | Nothing = cs stack Nothing Nothing
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
122 ... | Just d = get2SingleLinkedStack' {n} {m} stack cs
483
9098ec0a9e6b add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents: 478
diff changeset
123 where
499
2c125aa7a577 stack.agda leveled
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 496
diff changeset
124 get2SingleLinkedStack' : {n m : Level} {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
125 get2SingleLinkedStack' stack cs with (next d)
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
126 ... | Nothing = cs stack Nothing Nothing
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
127 ... | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
128
531
f6060e1bf900 add clearStack
ryokka
parents: 523
diff changeset
129 clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (SingleLinkedStack a -> t) -> t
f6060e1bf900 add clearStack
ryokka
parents: 523
diff changeset
130 clearSingleLinkedStack stack next = next (record {top = Nothing})
483
9098ec0a9e6b add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents: 478
diff changeset
131
9098ec0a9e6b add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents: 478
diff changeset
132
496
8e133a3938c0 fix agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 485
diff changeset
133 emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
134 emptySingleLinkedStack = record {top = Nothing}
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
135
509
51f0d5e5d1e5 stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 504
diff changeset
136 -----
51f0d5e5d1e5 stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 504
diff changeset
137 -- Basic stack implementations are specifications of a Stack
51f0d5e5d1e5 stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 504
diff changeset
138 --
515
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 511
diff changeset
139 singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
509
51f0d5e5d1e5 stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 504
diff changeset
140 singleLinkedStackSpec = record {
503
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
141 push = pushSingleLinkedStack
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
142 ; pop = popSingleLinkedStack
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
143 ; pop2 = pop2SingleLinkedStack
483
9098ec0a9e6b add getSingleLinkedStack,get2SingleLinkedStack. but get2SingleLinkedStack not working now
ryokka
parents: 478
diff changeset
144 ; get = getSingleLinkedStack
484
8a22cfd174bf pop2 and get2 in agda
ryokka
parents: 483
diff changeset
145 ; get2 = get2SingleLinkedStack
531
f6060e1bf900 add clearStack
ryokka
parents: 523
diff changeset
146 ; clear = clearSingleLinkedStack
503
413ce51da50b separate methods in stack.agda
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 502
diff changeset
147 }
161
db647f7ed2f6 Prove simple lemma in stack.agda
atton
parents: 158
diff changeset
148
515
54ff7a97aec1 fix findNode in Agda
ryokka
parents: 511
diff changeset
149 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
509
51f0d5e5d1e5 stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 504
diff changeset
150 createSingleLinkedStack = record {
51f0d5e5d1e5 stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 504
diff changeset
151 stack = emptySingleLinkedStack ;
51f0d5e5d1e5 stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 504
diff changeset
152 stackMethods = singleLinkedStackSpec
51f0d5e5d1e5 stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 504
diff changeset
153 }
51f0d5e5d1e5 stack proof on indeterminate stack state
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 504
diff changeset
154