Mercurial > hg > Papers > 2017 > ryokka-midterm
diff midterm/src/stack.agda.replace @ 7:c0a6124f436b default tip
delete natural deduction. add CbC,Agda more description
author | ryokka |
---|---|
date | Fri, 27 Oct 2017 17:06:15 +0900 |
parents | ead50a89470f |
children |
line wrap: on
line diff
--- a/midterm/src/stack.agda.replace Thu Oct 26 15:04:10 2017 +0900 +++ b/midterm/src/stack.agda.replace Fri Oct 27 17:06:15 2017 +0900 @@ -1,5 +1,12 @@ +record Stack {a t : Set} (stackImpl : Set) : Set where +field +stack : stackImpl +push : stackImpl -> a -> (stackImpl -> t) -> t +pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t +open Stack + pushStack : {a t : Set} -> Stack a -> a -> (Stack t -> t) -> t pushStack {a} {t} s0 d next = (push s0) (stack s0) d (\s1 -> next (record {stack = s1} )) popStack : {a t : Set} -> Stack a -> (Stack t -> t) -> t -popStack {a} {t} s0 next = (pop s0) (stack s0) (\s1 -> next s0) \ No newline at end of file +popStack {a} {t} s0 next = (pop s0) (stack s0) (\s1 -> next s0)