Mercurial > hg > Members > atton > agda-proofs

changeset 19:853318ff55f9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define output data segment
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 18 Dec 2016 07:59:51 +0000
parents 782a11f3eea4
children 4dd4400b48aa
files cbc/variable-tuple.agda
diffstat 1 files changed, 12 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/cbc/variable-tuple.agda	Sun Dec 18 06:41:39 2016 +0000
+++ b/cbc/variable-tuple.agda	Sun Dec 18 07:59:51 2016 +0000
@@ -4,6 +4,7 @@
 open import Data.String
 open import Data.List
 open import Data.Unit
+open import Data.Product
 open import Function using (_∘_)
 open import Relation.Binary.PropositionalEquality
 
@@ -48,14 +49,20 @@
 data CodeSegment : Set₁ where
   cs : Format -> Format -> CodeSegment
 
-ods : CodeSegment -> List Set
-ods (cs ids FEnd)         = []
-ods (cs ids (FSet s f))   = s ∷ (ods (cs ids f))
+csDouble : CodeSegment
+csDouble = cs double double
+
+ods : CodeSegment -> Set
+ods (cs ids FEnd)         = ⊤
+ods (cs ids (FSet s f))   = s × (ods (cs ids f))
+
+ods-double : ods csDouble
+ods-double = "hoge" , zero , tt
+
 
 ids : {A : Set} -> CodeSegment ->  Set
 ids {A} (cs i o) = DataSegment {A} i
 
-
-ids-double : {A : Set} {a : A} -> ids {A} (cs double double)
+ids-double : {A : Set} {a : A} -> ids {A} csDouble
 ids-double {_} {a}  =  \(s : String) -> \(n : ℕ) -> a