Mercurial > hg > Papers > 2020 > soto-midterm

comparison src/AgdaStackTest.agda @ 1:73127e0ab57c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
(none)
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 08 Sep 2020 18:38:08 +0900
parents
children
comparison
equal deleted inserted replaced
0:b919985837a3 1:73127e0ab57c
1 -- after push 1 and 2, pop2 get 1 and 2
2
3 testStack02 : {m : Level } -> ( Stack ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m}
4 testStack02 cs = pushStack createSingleLinkedStack 1 (\s -> pushStack s 2 cs)
5
6
7 testStack031 : (d1 d2 : ℕ ) -> Bool {Zero}
8 testStack031 2 1 = True
9 testStack031 _ _ = False
10
11 testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero}
12 testStack032 (Just d1) (Just d2) = testStack031 d1 d2
13 testStack032 _ _ = False
14
15 testStack03 : {m : Level } -> Stack ℕ (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m}
16 testStack03 s cs = pop2Stack s (\s d1 d2 -> cs d1 d2 )
17
18 testStack04 : Bool
19 testStack04 = testStack02 (\s -> testStack03 s testStack032)
20
21 testStack05 : testStack04 ≡ True
22 testStack05 = refl