Mercurial > hg > Papers > 2018 > ryokka-thesis
diff final_pre/src/AgdaStackTest.agda.replaced @ 7:28f900230c26
add final_pre
author | ryokka |
---|---|
date | Mon, 19 Feb 2018 23:32:24 +0900 |
parents | |
children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_pre/src/AgdaStackTest.agda.replaced Mon Feb 19 23:32:24 2018 +0900 @@ -0,0 +1,22 @@ +-- after push 1 and 2, pop2 get 1 and 2 + +testStack02 : {m : Level } @$\rightarrow$@ ( Stack @$\mathbb{N}$@ (SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ Bool {m} ) @$\rightarrow$@ Bool {m} +testStack02 cs = pushStack createSingleLinkedStack 1 (\s @$\rightarrow$@ pushStack s 2 cs) + + +testStack031 : (d1 d2 : $\mathbb{N}$ ) @$\rightarrow$@ Bool {Zero} +testStack031 2 1 = True +testStack031 _ _ = False + +testStack032 : (d1 d2 : Maybe @$\mathbb{N}$@) @$\rightarrow$@ Bool {Zero} +testStack032 (Just d1) (Just d2) = testStack031 d1 d2 +testStack032 _ _ = False + +testStack03 : {m : Level } @$\rightarrow$@ Stack @$\mathbb{N}$@ (SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ ((Maybe @$\mathbb{N}$@) @$\rightarrow$@ (Maybe @$\mathbb{N}$@) @$\rightarrow$@ Bool {m} ) @$\rightarrow$@ Bool {m} +testStack03 s cs = pop2Stack s (\s d1 d2 @$\rightarrow$@ cs d1 d2 ) + +testStack04 : Bool +testStack04 = testStack02 (\s @$\rightarrow$@ testStack03 s testStack032) + +testStack05 : testStack04 @$\equiv$@ True +testStack05 = refl