Mercurial > hg > Papers > 2018 > nozomi-master
view paper/src/Exec.agda @ 69:bda11534296f
Update pdf
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 04 Feb 2017 16:34:14 +0900 |
parents | 6d8825f3b051 |
children |
line wrap: on
line source
exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} {{_ : DataSegment I}} {{_ : DataSegment O}} -> CodeSegment I O -> Context -> Context exec {l} {{i}} {{o}} (cs b) c = set o c (b (get i c))