Mercurial > hg > Papers > 2018 > ryokka-sigos
view Paper/src/AgdaStackImpl.agda @ 8:35d15c091cfd
fix Makefile export .agda.replaced,and main document
author | ryokka |
---|---|
date | Mon, 23 Apr 2018 21:44:32 +0900 |
parents | 576637483425 |
children |
line wrap: on
line source
pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> 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} -> StackMethods {n} {m} a {t} (SingleLinkedStack a) singleLinkedStackSpec = record { push = pushSingleLinkedStack ; pop = popSingleLinkedStack } createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a) createSingleLinkedStack = record { stack = emptySingleLinkedStack ; tackMethods = singleLinkedStackSpec }