Mercurial > hg > Members > atton > agda-proofs

changeset 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 8ce6a3f51523
files cbc/stack-product.agda
diffstat 1 files changed, 7 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- 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
 
 
 {-