Mercurial > hg > Papers > 2019 > oshiro-thesis

comparison final_pre/src/stack.agda.replace @ 7:0e8b9646d43f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add final_pre
author e155702
date Sun, 17 Feb 2019 05:39:59 +0900
parents
children
comparison
equal deleted inserted replaced
6:8f5d263c219b 7:0e8b9646d43f
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
8 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
9 popSingleLinkedStack stack cs with (top stack)
10 ... | Nothing = cs stack Nothing
11 ... | Just d = cs stack1 (Just data1)
12 where
13 data1 = datum d
14 stack1 = record { top = (next d) }