Mercurial > hg > Papers > 2020 > soto-midterm

comparison src/AgdaStackImpl.agda.replaced @ 1:73127e0ab57c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
(none)
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 08 Sep 2020 18:38:08 +0900
parents
children
comparison
equal deleted inserted replaced
0:b919985837a3 1:73127e0ab57c
1 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ 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} @$\rightarrow$@ 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} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a)
16 createSingleLinkedStack = record {
17 stack = emptySingleLinkedStack ;
18 tackMethods = singleLinkedStackSpec
19 }