Mercurial > hg > Members > atton > agda-proofs

comparison cbc/subtype.agda @ 36:f0759cb39d37

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define codesegment using subtype
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Mon, 02 Jan 2017 04:40:48 +0000
parents
children
comparison
equal deleted inserted replaced
35:bf667ec8cba4 36:f0759cb39d37
1 module subtype where
2
3 open import Level
4 open import Function
5 open import Data.Nat hiding (_⊔_)
6 open import Data.Bool
7
8 data DataSegment (X : Set -> Set) : Set₁ where
9 ds : {x : Set} -> X x -> DataSegment X
10
11
12 record DS1 (A : Set) : Set where
13 field
14 counter : A -> ℕ
15
16 record DS2 (A : Set) : Set where
17 field
18 useSum : A -> Bool
19
20 record Context : Set where
21 field
22 loopCounter : ℕ
23 flag : Bool
24
25 instance
26 ds1 : DS1 Context
27 ds1 = record {counter = Context.loopCounter}
28
29 hoge : Context -> {{ins : DS1 Context}} -> DataSegment DS1
30 hoge _ {{i}} = ds i
31
32
33
34 data CodeSegment (I O : (Set -> Set)) : Set₁ where
35 cs : (DataSegment I -> DataSegment O) -> CodeSegment I O