Mercurial > hg > Members > Moririn

comparison src/parallel_execution/stack.agda @ 511:044c25475ed4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix stack.agda
author mir3636
date Thu, 04 Jan 2018 14:42:21 +0900
parents 51f0d5e5d1e5
children 54ff7a97aec1
comparison
equal deleted inserted replaced
510:647716041772 511:044c25475ed4
93 ... | Just d = pop2SingleLinkedStack' {n} {m} stack cs 93 ... | Just d = pop2SingleLinkedStack' {n} {m} stack cs
94 where 94 where
95 pop2SingleLinkedStack' : {n m : Level } {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t 95 pop2SingleLinkedStack' : {n m : Level } {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
96 pop2SingleLinkedStack' stack cs with (next d) 96 pop2SingleLinkedStack' stack cs with (next d)
97 ... | Nothing = cs stack Nothing Nothing 97 ... | Nothing = cs stack Nothing Nothing
98 ... | Just d1 = cs (record {top = (next d)}) (Just (datum d)) (Just (datum d1)) 98 ... | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
99 99
100 100
101 getSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t 101 getSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
102 getSingleLinkedStack stack cs with (top stack) 102 getSingleLinkedStack stack cs with (top stack)
103 ... | Nothing = cs stack Nothing 103 ... | Nothing = cs stack Nothing