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