# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1483517762 0
# Node ID 08b695ca359c83cddca27a012ae33ec06711ebfb
# Parent  72cf35fb82af48b3d2de4244ce57e06c748cdf7a
Cannot compose code segments has another type signature ...

diff -r 72cf35fb82af -r 08b695ca359c cbc/named-product.agda
--- a/cbc/named-product.agda	Wed Jan 04 02:26:58 2017 +0000
+++ b/cbc/named-product.agda	Wed Jan 04 08:16:02 2017 +0000
@@ -3,7 +3,8 @@
 open import Function
 open import Data.Bool
 open import Data.Nat
-open import Data.String hiding (_++_)
+open import Data.Nat.Show
+open import Data.String hiding (_++_ ; show)
 open import Data.List
 open import Relation.Binary.PropositionalEquality
 
@@ -91,3 +92,13 @@
 
 apply-sample : Context
 apply-sample = exec comp-sample firstContext
+
+
+updateSignature : SignatureWithNum -> SignatureWithNum
+updateSignature record { signature = signature ; num = num } = record { signature = (Data.String._++_) signature (show num ) ; num = num}
+
+csUpdateSignature : basicCS SignatureWithNum SignatureWithNum
+csUpdateSignature = cs updateSignature
+
+comp-sample-2 : CodeSegment LoopCounter SignatureWithNum ?
+comp-sample-2 = csUpdateSignature ◎ csInc