Mercurial > hg > Papers > 2017 > atton-master
diff paper/src/AgdaNPushNPop.agda @ 67:ec6799ca9d42
Add proof description
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 04 Feb 2017 16:19:23 +0900 (2017-02-04) |
parents | |
children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/AgdaNPushNPop.agda Sat Feb 04 16:19:23 2017 +0900 @@ -0,0 +1,13 @@ +n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta +n-push {{mm}} (zero) = M.cs {{mm}} {{mm}} id +n-push {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-push {m} {{mm}} n) (pushOnce m)) + +n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta +n-pop {{mm}} (zero) = M.cs {{mm}} {{mm}} id +n-pop {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-pop {m} {{mm}} n) (popOnce m)) + +pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁ +pop-n-push-type n cn ce s = M.exec (M.csComp {meta} (M.cs popOnce) (n-push {meta} (suc n))) meta + ≡ M.exec (n-push {meta} n) meta + where + meta = id-meta cn ce s