comparison final_main/src/Exec.agda @ 0:83f997abf3b5

first commit
author e155702
date Thu, 14 Feb 2019 16:51:50 +0900
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:83f997abf3b5
1 exec : {l1 l2 : Level} {I : Set l1} {O : Set l2}
2 {{_ : DataSegment I}} {{_ : DataSegment O}}
3 -> CodeSegment I O -> Context -> Context
4 exec {l} {{i}} {{o}} (cs b) c = set o c (b (get i c))
5