Mercurial > hg > Papers > 2022 > soto-sigos

comparison Paper/src/AgdaStackImpl.agda @ 0:14a0e409d574

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ADD fast commit
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 24 Apr 2022 23:13:44 +0900
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:14a0e409d574
1 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
2 pushSingleLinkedStack stack datum next = next stack1
3 where
4 element = cons datum (top stack)
5 stack1 = record {top = Just element}
6
7 -- Basic stack implementations are specifications of a Stack
8
9 singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
10 singleLinkedStackSpec = record {
11 push = pushSingleLinkedStack
12 ; pop = popSingleLinkedStack
13 }
14
15 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
16 createSingleLinkedStack = record {
17 stack = emptySingleLinkedStack ;
18 tackMethods = singleLinkedStackSpec
19 }