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 } -> Maybe (Element ℕ)
testStack07 = pushSingleLinkedStack emptySingleLinkedStack 1 (\s -> pushSingleLinkedStack s 2 (\s -> top s))

testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1
  $ \s -> pushSingleLinkedStack s 2
  $ \s -> pushSingleLinkedStack s 3
  $ \s -> pushSingleLinkedStack s 4
  $ \s -> pushSingleLinkedStack s 5
  $ \s -> top s


testStack10 = pushStack emptySingleLinkedStack 1
  $ \s -> pushStack 2
  $ \s -> pushStack 3
  $ \s -> pushStack 4
  $ \s -> pushStack 5
  $ \s -> top s