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