changeset 58:b7493ee642de

Trying define maybe-subtype...
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 12 Jan 2017 01:05:06 +0000
parents 75f9f71f364a
children 352e8a724829
files cbc/maybe-subtype-sample.agda
diffstat 1 files changed, 13 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /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