Mercurial > hg > Members > atton > agda-proofs

diff cbc/stack-product.agda @ 54:fa95e3070138

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define SingleLinkedStack using subtype
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Wed, 11 Jan 2017 10:56:13 +0000
parents b8e606ab3a0b
children bd428bd6b394
line wrap: on
line diff
--- a/cbc/stack-product.agda	Tue Jan 10 09:07:07 2017 +0000
+++ b/cbc/stack-product.agda	Wed Jan 11 10:56:13 2017 +0000
@@ -108,7 +108,7 @@
   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
+    push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , ? {- n-push -}) -- needs subtype
 
 
 {-