Mercurial > hg > Papers > 2018 > nozomi-master
view paper/src/MetaCodeSegment.agda @ 69:bda11534296f
Update pdf
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 04 Feb 2017 16:34:14 +0900 |
parents | a40033d3e10f |
children |
line wrap: on
line source
data CodeSegment {l1 l2 : Level} (A : Set l1) (B : Set l2) : Set (l ⊔ l1 ⊔ l2) where cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B