Mercurial > hg > Papers > 2018 > nozomi-master
annotate paper/src/MetaDataSegment.agda @ 69:bda11534296f
Update pdf
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 04 Feb 2017 16:34:14 +0900 |
parents | 3981580ece72 |
children |
rev | line source |
---|---|
61
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 module subtype {l : Level} (Context : Set l) where |
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 |
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 record DataSegment {ll : Level} (A : Set ll) : Set (l ⊔ ll) where |
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 field |
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 get : Context -> A |
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 set : Context -> A -> Context |
3981580ece72
Add Meta DataSegment description
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 |