Papers/2019/oshiro-thesis: final_main/src/AgdaStackTest.agda.replaced comparison

first commit

comparison

equal deleted inserted replaced

--1:000000000000
+:83f997abf3b5
+-- 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

Mercurial > hg > Papers > 2019 > oshiro-thesis