Mercurial > hg > Papers > 2020 > ryokka-master
diff paper/src/AgdaStackTest.agda @ 2:c7acb9211784
add code, figure. and paper fix content
author | ryokka |
---|---|
date | Mon, 27 Jan 2020 20:41:36 +0900 |
parents | |
children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/AgdaStackTest.agda Mon Jan 27 20:41:36 2020 +0900 @@ -0,0 +1,22 @@ +-- after push 1 and 2, pop2 get 1 and 2 + +testStack02 : {m : Level } -> ( Stack ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m} +testStack02 cs = pushStack createSingleLinkedStack 1 (\s -> pushStack s 2 cs) + + +testStack031 : (d1 d2 : ℕ ) -> Bool {Zero} +testStack031 2 1 = True +testStack031 _ _ = False + +testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero} +testStack032 (Just d1) (Just d2) = testStack031 d1 d2 +testStack032 _ _ = False + +testStack03 : {m : Level } -> Stack ℕ (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m} +testStack03 s cs = pop2Stack s (\s d1 d2 -> cs d1 d2 ) + +testStack04 : Bool +testStack04 = testStack02 (\s -> testStack03 s testStack032) + +testStack05 : testStack04 ≡ True +testStack05 = refl