Mercurial > hg > Gears > GearsAgda
diff stack.agda @ 574:70b09cbefd45
add queue.agda
author | ryokka |
---|---|
date | Thu, 16 Aug 2018 18:22:08 +0900 |
parents | 988c12d7f887 |
children | 73fc32092b64 |
line wrap: on
line diff
--- a/stack.agda Sun May 06 19:35:38 2018 +0900 +++ b/stack.agda Thu Aug 16 18:22:08 2018 +0900 @@ -25,7 +25,7 @@ Nothing : Maybe a Just : a -> Maybe a -record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where +record StackMethods {n m : Level } (a : Set n ) {t : Set m } (stackImpl : Set n ) : Set (m Level.⊔ n) where field push : stackImpl -> a -> (stackImpl -> t) -> t pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t