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