Mercurial > hg > Members > atton > agda-proofs

changeset 45:08b695ca359c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Cannot compose code segments has another type signature ...
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Wed, 04 Jan 2017 08:16:02 +0000
parents 72cf35fb82af
children af1fe3bd9f1e
files cbc/named-product.agda
diffstat 1 files changed, 12 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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