Mercurial > hg > Members > atton > agda-proofs

annotate cbc/maybe-subtype-sample.agda @ 59:352e8a724829

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define maybe-subtype......
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 12 Jan 2017 02:48:09 +0000
parents b7493ee642de
children bd428bd6b394
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
59
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
1 module maybe-subtype-sample (A : Set) where
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
2
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
3 open import Level
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
4 open import Function using (id)
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
5 open import Relation.Binary.PropositionalEquality
58
b7493ee642de Trying define maybe-subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
59
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
7
58
b7493ee642de Trying define maybe-subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
59
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
9 open import maybe-subtype A
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
10 open import subtype (Context A) as M
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
11 open import subtype A as N
58
b7493ee642de Trying define maybe-subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
b7493ee642de Trying define maybe-subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 return : {_ : Context A} {_ : Meta (Context A)} {{_ : N.DataSegment A}} {{_ : M.DataSegment A}} -> A -> Meta A
59
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
14 return {c} {mc} {{nd}} {{md}} a = record {context = record {maybeElem = just a}}
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
15
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
16 fmap' : {B : Set} {{_ : M.DataSegment (Context A)}} {{_ : M.DataSegment (Context B)}} -> (A -> B) -> Context A -> Context B
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
17 fmap' f record { maybeElem = (just x) } = record {maybeElem = just (f x)}
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
18 fmap' f record { maybeElem = nothing } = record {maybeElem = nothing}
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
19
58
b7493ee642de Trying define maybe-subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
b7493ee642de Trying define maybe-subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
59
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
22 fmap : {c : Context A} {B : Set}
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
23 {{_ : N.DataSegment A}} {{_ : N.DataSegment B}} {{_ : M.DataSegment (Context A)}} {{_ : M.DataSegment (Context B)}}
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
24 -> N.CodeSegment A B -> M.CodeSegment (Context A) (Context B)
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
25 fmap {c} {B} {{na}} {{nb}} {{ma}} {{mb}} (N.cs f) = M.cs {{ma}} (fmap' {B} {{ma}} {{mb}} f)
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
26
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
27
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
28
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
29
352e8a724829 Trying define maybe-subtype......
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 58
diff changeset
30