Mercurial > hg > Members > atton > agda-proofs

comparison cbc/subtype.agda @ 55:81c6779583b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add push-sample
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Wed, 11 Jan 2017 13:37:23 +0000
parents fa95e3070138
children bd428bd6b394
comparison
equal deleted inserted replaced
54:fa95e3070138 55:81c6779583b6
12 12
13 data CodeSegment {l1 l2 : Level} (A : Set l1) (B : Set l2) : Set (l ⊔ l1 ⊔ l2) where 13 data CodeSegment {l1 l2 : Level} (A : Set l1) (B : Set l2) : Set (l ⊔ l1 ⊔ l2) where
14 cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B 14 cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B
15 15
16 16
17 exec : {I O : Set} {{_ : DataSegment I}} {{_ : DataSegment O}} -> CodeSegment I O -> Context -> Context 17 exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} {{_ : DataSegment I}} {{_ : DataSegment O}}
18 -> CodeSegment I O -> Context -> Context
18 exec {l} {{i}} {{o}} (cs b) c = set o c (b (get i c)) 19 exec {l} {{i}} {{o}} (cs b) c = set o c (b (get i c))
19 20
20 21
21 comp : {con : Context} -> {l1 l2 l3 l4 : Level} 22 comp : {con : Context} -> {l1 l2 l3 l4 : Level}
22 {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4} 23 {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4}