--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaDebug.agda.replaced	Mon Jan 27 20:41:36 2020 +0900
@@ -0,0 +1,32 @@
+open import Level renaming (suc to succ ; zero to Zero )
+
+module AgdaDebug where
+
+open import stack
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Data.Nat
+open import Function
+
+
+open SingleLinkedStack
+open Stack
+
+testStack07 : {m : Level } @$\rightarrow$@ Maybe (Element @$\mathbb{N}$@)
+testStack07 = pushSingleLinkedStack emptySingleLinkedStack 1 (\s @$\rightarrow$@ pushSingleLinkedStack s 2 (\s @$\rightarrow$@ top s))
+
+testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1
+  $ \s @$\rightarrow$@ pushSingleLinkedStack s 2
+  $ \s @$\rightarrow$@ pushSingleLinkedStack s 3
+  $ \s @$\rightarrow$@ pushSingleLinkedStack s 4
+  $ \s @$\rightarrow$@ pushSingleLinkedStack s 5
+  $ \s @$\rightarrow$@ top s
+
+
+testStack10 = pushStack emptySingleLinkedStack 1
+  $ \s @$\rightarrow$@ pushStack 2
+  $ \s @$\rightarrow$@ pushStack 3
+  $ \s @$\rightarrow$@ pushStack 4
+  $ \s @$\rightarrow$@ pushStack 5
+  $ \s @$\rightarrow$@ top s