Mercurial > hg > Papers > 2018 > nozomi-master
view paper/src/Exec.agda @ 63:6d8825f3b051
Add example of meta code segment execution
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 03 Feb 2017 11:59:41 +0900 |
parents | |
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))