Mercurial > hg > Members > atton > agda-proofs

changeset 20:4dd4400b48aa

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define code segment execution
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 18 Dec 2016 08:10:02 +0000
parents 853318ff55f9
children afb2304be45b
files cbc/variable-tuple.agda
diffstat 1 files changed, 4 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- 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
+