Mercurial > hg > Gears > GearsAgda

diff stackTest.agda @ 538:5c001e8ba0d5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add redBlackTreeTest.agda test5,test51. but not work
author ryokka
date Wed, 10 Jan 2018 17:38:24 +0900
parents fffeaf0b0024
children 429ece770187
line wrap: on
line diff
--- a/stackTest.agda	Wed Jan 10 15:44:13 2018 +0900
+++ b/stackTest.agda	Wed Jan 10 17:38:24 2018 +0900
@@ -61,6 +61,15 @@
 testStack05 : testStack04 ≡ True
 testStack05 = refl
 
+testStack06 : {m : Level } -> Maybe (Element ℕ)
+testStack06 = pushStack createSingleLinkedStack 1 (
+   \s -> pushStack s 2 (\s -> top (stack s)))
+
+testStack07 : {m : Level } -> Maybe (Element ℕ)
+testStack07 = pushSingleLinkedStack emptySingleLinkedStack 1 (
+   \s -> pushSingleLinkedStack s 2 (\s -> top s))
+
+
 ------
 --
 -- proof of properties with indefinite state of stack