Mercurial > hg > Members > atton > agda-proofs

comparison cbc/stack-product.agda @ 29:b8e606ab3a0b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define n-push...
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Fri, 23 Dec 2016 16:14:36 +0000
parents 67978ba63a6f
children fa95e3070138
comparison
equal deleted inserted replaced
28:67978ba63a6f 29:b8e606ab3a0b
1 module stack-product where 1 module stack-product where
2 2
3 open import product 3 open import product
4 open import Data.Product 4 open import Data.Product
5 open import Data.Nat
5 open import Function using (id) 6 open import Function using (id)
6 open import Relation.Binary.PropositionalEquality 7 open import Relation.Binary.PropositionalEquality
7 8
8 -- definition based from Gears(209:5708390a9d88) src/parallel_execution 9 -- definition based from Gears(209:5708390a9d88) src/parallel_execution
9 goto = executeCS 10 goto = executeCS
100 101
101 lemma : {A : Set} {a : A} -> goto (test03 ◎ test02 ◎ test01) a ≡ False 102 lemma : {A : Set} {a : A} -> goto (test03 ◎ test02 ◎ test01) a ≡ False
102 lemma = refl 103 lemma = refl
103 104
104 105
106 n-push : {A : Set} {a : A} -> CodeSegment (ℕ × SingleLinkedStack A) (ℕ × SingleLinkedStack A)
107 n-push {A} {a} = cs (push {A} {a})
108 where
109 push : {A : Set} {a : A} -> (ℕ × SingleLinkedStack A) -> (ℕ × SingleLinkedStack A)
110 push {A} {a} (zero , s) = (zero , s)
111 push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , {!!} {- n-push -}) -- needs subtype
105 112
106 113
107 {- 114 {-
108 115
109 n-push : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A 116 n-push : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A