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 -- 以下よりメタメタレベルのプログラムを記述できる