|
1
|
1 open import Level renaming (suc to succ ; zero to Zero )
|
|
|
2
|
|
|
3 module AgdaDebug where
|
|
|
4
|
|
|
5 open import stack
|
|
|
6
|
|
|
7 open import Relation.Binary.PropositionalEquality
|
|
|
8 open import Relation.Binary.Core
|
|
|
9 open import Data.Nat
|
|
|
10 open import Function
|
|
|
11
|
|
|
12
|
|
|
13 open SingleLinkedStack
|
|
|
14 open Stack
|
|
|
15
|
|
|
16 testStack07 : {m : Level } @$\rightarrow$@ Maybe (Element @$\mathbb{N}$@)
|
|
|
17 testStack07 = pushSingleLinkedStack emptySingleLinkedStack 1 (\s @$\rightarrow$@ pushSingleLinkedStack s 2 (\s @$\rightarrow$@ top s))
|
|
|
18
|
|
|
19 testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1
|
|
|
20 $ \s @$\rightarrow$@ pushSingleLinkedStack s 2
|
|
|
21 $ \s @$\rightarrow$@ pushSingleLinkedStack s 3
|
|
|
22 $ \s @$\rightarrow$@ pushSingleLinkedStack s 4
|
|
|
23 $ \s @$\rightarrow$@ pushSingleLinkedStack s 5
|
|
|
24 $ \s @$\rightarrow$@ top s
|
|
|
25
|
|
|
26
|
|
|
27 testStack10 = pushStack emptySingleLinkedStack 1
|
|
|
28 $ \s @$\rightarrow$@ pushStack 2
|
|
|
29 $ \s @$\rightarrow$@ pushStack 3
|
|
|
30 $ \s @$\rightarrow$@ pushStack 4
|
|
|
31 $ \s @$\rightarrow$@ pushStack 5
|
|
|
32 $ \s @$\rightarrow$@ top s
|
