|
57
|
1 module maybe-subtype (A : Set) where
|
|
|
2
|
|
|
3 open import Level
|
|
|
4 open import Function using (id)
|
|
|
5 open import Relation.Binary.PropositionalEquality
|
|
|
6
|
|
|
7 data Maybe (A : Set) : Set where
|
|
|
8 nothing : Maybe A
|
|
|
9 just : A -> Maybe A
|
|
|
10
|
|
|
11
|
|
|
12 record Context (A : Set) : Set where
|
|
|
13 field
|
|
|
14 maybeElem : Maybe A
|
|
|
15
|
|
|
16 open import subtype (Context A) as N
|
|
|
17
|
|
|
18
|
|
|
19 record Meta (A : Set) : Set where
|
|
|
20 field
|
|
|
21 context : Context A
|
|
|
22
|
|
|
23
|
|
|
24 open import subtype (Meta A) as M
|
|
|
25
|
|
|
26 instance
|
|
|
27 MetaIsMetaDataSegment : M.DataSegment (Meta A)
|
|
|
28 MetaIsMetaDataSegment = record {get = (\mc -> mc) ; set = (\_ mc -> mc)}
|
|
|
29 ContextIsMetaDataSegment : M.DataSegment (Context A)
|
|
|
30 ContextIsMetaDataSegment = record {get = Meta.context ; set = (\mc c -> record mc {context = c})}
|
|
|
31
|
