Mercurial > hg > Members > atton > agda-proofs

comparison 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
comparison
equal deleted inserted replaced
53:6af88ee5c4ca 54:fa95e3070138
106 n-push : {A : Set} {a : A} -> CodeSegment (ℕ × SingleLinkedStack A) (ℕ × SingleLinkedStack A) 106 n-push : {A : Set} {a : A} -> CodeSegment (ℕ × SingleLinkedStack A) (ℕ × SingleLinkedStack A)
107 n-push {A} {a} = cs (push {A} {a}) 107 n-push {A} {a} = cs (push {A} {a})
108 where 108 where
109 push : {A : Set} {a : A} -> (ℕ × SingleLinkedStack A) -> (ℕ × SingleLinkedStack A) 109 push : {A : Set} {a : A} -> (ℕ × SingleLinkedStack A) -> (ℕ × SingleLinkedStack A)
110 push {A} {a} (zero , s) = (zero , s) 110 push {A} {a} (zero , s) = (zero , s)
111 push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , {!!} {- n-push -}) -- needs subtype 111 push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , ? {- n-push -}) -- needs subtype
112 112
113 113
114 {- 114 {-
115 115
116 n-push : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A 116 n-push : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A