Mercurial > hg > Papers > 2020 > ryokka-master

comparison paper/src/AgdaStackImpl.agda @ 2:c7acb9211784

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add code, figure. and paper fix content
author ryokka
date Mon, 27 Jan 2020 20:41:36 +0900
parents
children
comparison
equal deleted inserted replaced
1:ee44dbda6bd3 2:c7acb9211784
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 }