-- after push 1 and 2, pop2 get 1 and 2

testStack02 : {m : Level } ->  ( Stack  ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m}
testStack02 cs = pushStack createSingleLinkedStack 1 (\s -> pushStack s 2 cs)


testStack031 : (d1 d2 : ℕ ) -> Bool {Zero}
testStack031 2 1 = True
testStack031 _ _ = False

testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero}
testStack032  (Just d1) (Just d2) = testStack031 d1 d2
testStack032  _ _ = False

testStack03 : {m : Level } -> Stack  ℕ (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m}
testStack03 s cs = pop2Stack s (\s d1 d2 -> cs d1 d2 )

testStack04 : Bool
testStack04 = testStack02 (\s -> testStack03 s testStack032)

testStack05 : testStack04 ≡ True
testStack05 = refl