Mercurial > hg > Papers > 2022 > soto-sigos
comparison Paper/src/Exec.agda.replaced @ 0:14a0e409d574
ADD fast commit
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Apr 2022 23:13:44 +0900 |
| parents | |
| children |
comparison
equal
deleted
inserted
replaced
| -1:000000000000 | 0:14a0e409d574 |
|---|---|
| 1 exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} | |
| 2 {{_ : DataSegment I}} {{_ : DataSegment O}} | |
| 3 !$\rightarrow$! CodeSegment I O !$\rightarrow$! Context !$\rightarrow$! Context | |
| 4 exec {l} {{i}} {{o}} (cs b) c = set o c (b (get i c)) | |
| 5 |