Mercurial > hg > Papers > 2018 > ryokka-thesis
comparison final_pre/src/stack.agda.replace @ 7:28f900230c26
add final_pre
author | ryokka |
---|---|
date | Mon, 19 Feb 2018 23:32:24 +0900 |
parents | |
children |
comparison
equal
deleted
inserted
replaced
6:d927f6b3d2b3 | 7:28f900230c26 |
---|---|
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) } |