Mercurial > hg > Papers > 2020 > ryokka-master

comparison paper/src/AgdaStackTest.agda.replaced @ 2:c7acb9211784

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add code, figure. and paper fix content
author ryokka
date Mon, 27 Jan 2020 20:41:36 +0900
parents
children
comparison
equal deleted inserted replaced
1:ee44dbda6bd3 2:c7acb9211784
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