Mercurial > hg > GearsTemplate

changeset 500:6d984ea42fd2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix proof
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 01 Jan 2018 11:19:14 +0900
parents 2c125aa7a577
children 55077dd40a51
files src/parallel_execution/stack.agda
diffstat 1 files changed, 6 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/stack.agda	Mon Jan 01 09:34:46 2018 +0900
+++ b/src/parallel_execution/stack.agda	Mon Jan 01 11:19:14 2018 +0900
@@ -146,19 +146,19 @@
 lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False
 lemma = refl
 
--- after push 1 and 2, pop2 get 1 and 2
-
 testStack01 : {n : Level } {a : Set n} -> a -> Bool
 testStack01 v = pushStack createSingleLinkedStack v (
    \s -> popStack s (\s1 d1 -> True))
 
-testStack02 : (Stack (SingleLinkedStack ℕ) -> Bool) -> Bool
+-- after push 1 and 2, pop2 get 1 and 2
+
+testStack02 : ( Stack (SingleLinkedStack ℕ) -> Bool) -> Bool
 testStack02 cs = pushStack createSingleLinkedStack 1 (
    \s -> pushStack s 2 cs)
 
 
 testStack031 : (d1 d2 : ℕ ) -> Bool {Zero}
-testStack031 1 2 = True
+testStack031 2 1 = True
 testStack031 _ _ = False
 
 testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero}
@@ -172,8 +172,8 @@
 testStack04 : Bool
 testStack04 = testStack02 (\s -> testStack03 s testStack032)
 
-testStack05 : Set (succ Zero)
-testStack05 = testStack04 ≡ True
+testStack05 : testStack04 ≡ True
+testStack05 = refl
 
 id : {n : Level} {A : Set n} -> A -> A
 id a = a