Mercurial > hg > Members > Moririn

comparison src/parallel_execution/stack.agda @ 165:bf26f1105862

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Generalize lemma
author atton
date Thu, 17 Nov 2016 18:34:39 +0000
parents b0c6e0392b00
children b3be97ba0782
comparison
equal deleted inserted replaced
164:b0c6e0392b00 165:bf26f1105862
75 75
76 76
77 test02 : {a : Set} -> SingleLinkedStack a -> Bool 77 test02 : {a : Set} -> SingleLinkedStack a -> Bool
78 test02 stack = (popSingleLinkedStack stack) test01 78 test02 stack = (popSingleLinkedStack stack) test01
79 79
80 test03 : Bool 80 test03 : {a : Set} -> a -> Bool
81 test03 = pushSingleLinkedStack emptySingleLinkedStack (cons True Nothing) test02 -- ok 81 test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02
82 --test03 = pushSingleLinkedStack emptySingleLinkedStack (False) test02 -- ok
83 82
84 83
85 lemma : test03 ≡ False 84 lemma : {A : Set} {a : A} -> test03 a ≡ False
86 lemma = refl 85 lemma = refl