Mercurial > hg > Papers > 2018 > nozomi-master
comparison paper/src/MetaMetaDataSegment.agda @ 100:ebe838b83ada
Self review
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 12 Feb 2017 11:52:20 +0900 |
parents | 6d8825f3b051 |
children |
comparison
equal
deleted
inserted
replaced
99:a891d7551bbf | 100:ebe838b83ada |
---|---|
1 ... | 1 -- 上で各 DataSegement の定義を行なっているとする |
2 open import subtype Context as N | 2 open import subtype Context as N -- Meta Datasegment を定義 |
3 | 3 |
4 -- Meta DataSegment を持つ Meta Meta DataSegment を定義できる | |
4 record Meta : Set where | 5 record Meta : Set where |
5 field | 6 field |
6 context : Context | 7 context : Context |
7 c' : Int | 8 c' : Int |
8 next : N.CodeSegment Context Context | 9 next : N.CodeSegment Context Context |
9 | 10 |
10 open import subtype Meta as M | 11 open import subtype Meta as M |
11 ... | 12 -- 以下よりメタメタレベルのプログラムを記述できる |