# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1484183106 0
# Node ID b7493ee642de9720fd19c6e99a934755dae3b2cb
# Parent  75f9f71f364a0ceca33eab17d8868d1b1b953f7f
Trying define maybe-subtype...

diff -r 75f9f71f364a -r b7493ee642de cbc/maybe-subtype-sample.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbc/maybe-subtype-sample.agda	Thu Jan 12 01:05:06 2017 +0000
@@ -0,0 +1,13 @@
+module maybe-subtype-sample where
+
+open import subtype 
+
+
+return : {_ : Context A} {_ : Meta (Context A)} {{_ : N.DataSegment A}} {{_ : M.DataSegment A}} -> A -> Meta A
+return {c} {mc} {{nd}} {{md}} a = record {context = con ; maybeElem = just a}
+  where
+    con = record { elem = a }
+
+
+fmap : {B : Set} {{_ : M.DataSegment A}} {{_ : M.DataSegment B}} -> M.CodeSegment A B -> Meta (Context A) -> Meta (Context B)
+fmap code x = {!!} -- exec code x