Mercurial > hg > Papers > 2022 > soto-sigos

comparison Paper/src/AgdaInterface.agda @ 0:14a0e409d574

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ADD fast commit
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 24 Apr 2022 23:13:44 +0900
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:14a0e409d574
1 record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
2 field
3 push : stackImpl -> a -> (stackImpl -> t) -> t
4 pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t
5 open StackMethods
6
7 record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
8 field
9 stack : si
10 stackMethods : StackMethods {n} {m} a {t} si
11 pushStack : a -> (Stack a si -> t) -> t
12 pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
13 popStack : (Stack a si -> Maybe a -> t) -> t
14 popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
15 open Stack