Mercurial > hg > Papers > 2020 > soto-midterm
view src/AgdaStackImpl.agda.replaced @ 1:73127e0ab57c
(none)
author | soto@cr.ie.u-ryukyu.ac.jp |
---|---|
date | Tue, 08 Sep 2020 18:38:08 +0900 |
parents | |
children |
line wrap: on
line source
pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t pushSingleLinkedStack stack datum next = next stack1 where element = cons datum (top stack) stack1 = record {top = Just element} -- Basic stack implementations are specifications of a Stack singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a) singleLinkedStackSpec = record { push = pushSingleLinkedStack ; pop = popSingleLinkedStack } createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a) createSingleLinkedStack = record { stack = emptySingleLinkedStack ; tackMethods = singleLinkedStackSpec }