Mercurial > hg > Members > atton > agda-proofs

comparison cbc/maybe-subtype.agda @ 60:bd428bd6b394

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define n-push/n-pop
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sat, 14 Jan 2017 00:00:40 +0000
parents 352e8a724829
children
comparison
equal deleted inserted replaced
59:352e8a724829 60:bd428bd6b394
1 module maybe-subtype (A : Set) where
2
3 open import Level 1 open import Level
2 open import Data.Maybe
4 open import Function using (id) 3 open import Function using (id)
5 open import Relation.Binary.PropositionalEquality 4 open import Relation.Binary.PropositionalEquality
6 5
7 data Maybe (A : Set) : Set where 6 module maybe-subtype (A : Set) where
8 nothing : Maybe A
9 just : A -> Maybe A
10 7
11 8
12 record Context (A : Set) : Set where 9 record Context : Set where
13 field
14 maybeElem : Maybe A
15 10
16 open import subtype (Context A) as N 11 open import subtype Context as N
17 12
18 13
19 record Meta (A : Set) : Set where 14 record Meta (A : Set) : Set where
20 field 15 field
21 context : Context A 16 context : Context
17 maybeElem : Maybe A
22 18
23 19
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