# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1482509676 0
# Node ID b8e606ab3a0b3e9602a41ded90fde34a2676908a
# Parent  67978ba63a6f12503d2ea3188f3cd044c256efa4
Trying define n-push...

diff -r 67978ba63a6f -r b8e606ab3a0b cbc/stack-product.agda
--- a/cbc/stack-product.agda	Fri Dec 23 10:43:23 2016 +0000
+++ b/cbc/stack-product.agda	Fri Dec 23 16:14:36 2016 +0000
@@ -2,6 +2,7 @@
 
 open import product
 open import Data.Product
+open import Data.Nat
 open import Function using (id)
 open import Relation.Binary.PropositionalEquality
 
@@ -102,6 +103,12 @@
 lemma = refl
 
 
+n-push : {A : Set} {a : A} -> CodeSegment (ℕ  × SingleLinkedStack A) (ℕ × SingleLinkedStack A)
+n-push {A} {a} = cs (push {A} {a})
+  where
+    push : {A : Set} {a : A} -> (ℕ × SingleLinkedStack A) -> (ℕ × SingleLinkedStack A)
+    push {A} {a} (zero  , s) = (zero , s)
+    push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , {!!} {- n-push -}) -- needs subtype
 
 
 {-