|
1
|
1 -- after push 1 and 2, pop2 get 1 and 2
|
|
|
2
|
|
|
3 testStack02 : {m : Level } -> ( Stack ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m}
|
|
|
4 testStack02 cs = pushStack createSingleLinkedStack 1 (\s -> pushStack s 2 cs)
|
|
|
5
|
|
|
6
|
|
|
7 testStack031 : (d1 d2 : ℕ ) -> Bool {Zero}
|
|
|
8 testStack031 2 1 = True
|
|
|
9 testStack031 _ _ = False
|
|
|
10
|
|
|
11 testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero}
|
|
|
12 testStack032 (Just d1) (Just d2) = testStack031 d1 d2
|
|
|
13 testStack032 _ _ = False
|
|
|
14
|
|
|
15 testStack03 : {m : Level } -> Stack ℕ (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m}
|
|
|
16 testStack03 s cs = pop2Stack s (\s d1 d2 -> cs d1 d2 )
|
|
|
17
|
|
|
18 testStack04 : Bool
|
|
|
19 testStack04 = testStack02 (\s -> testStack03 s testStack032)
|
|
|
20
|
|
|
21 testStack05 : testStack04 ≡ True
|
|
|
22 testStack05 = refl
|
