Mercurial > hg > Papers > 2020 > ryokka-master

annotate paper/src/PushPopType.agda.replaced @ 2:c7acb9211784

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add code, figure. and paper fix content
author ryokka
date Mon, 27 Jan 2020 20:41:36 +0900
parents
children 196ba119ca89
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
2
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
1 pushOnce : Meta @$\rightarrow$@ Meta
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
2 pushOnce m = M.exec pushSingleLinkedStackCS m
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
3
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
4 popOnce : Meta @$\rightarrow$@ Meta
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
5 popOnce m = M.exec popSingleLinkedStackCS m
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
6
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
7 push-pop-type : Meta @$\rightarrow$@ Set@$\text{1}$@
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
8 push-pop-type meta =
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
9 M.exec (M.csComp (M.cs popOnce) (M.cs pushOnce)) meta @$\equiv$@ meta