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