# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1482048602 0
# Node ID 4dd4400b48aa7a23deb4646386c219462376bba3
# Parent  853318ff55f979a2ae57369b4b67b36c0e0f0e47
Define code segment execution

diff -r 853318ff55f9 -r 4dd4400b48aa cbc/variable-tuple.agda
--- a/cbc/variable-tuple.agda	Sun Dec 18 07:59:51 2016 +0000
+++ b/cbc/variable-tuple.agda	Sun Dec 18 08:10:02 2016 +0000
@@ -66,3 +66,7 @@
 ids-double : {A : Set} {a : A} -> ids {A} csDouble
 ids-double {_} {a}  =  \(s : String) -> \(n : ℕ) -> a
 
+
+executeCS : (cs : CodeSegment) -> Set
+executeCS c = ids {ods c} c
+