Mercurial > hg > Members > atton > agda-proofs

diff 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
line wrap: on
line diff
--- a/cbc/subtype.agda	Wed Jan 11 10:56:13 2017 +0000
+++ b/cbc/subtype.agda	Wed Jan 11 13:37:23 2017 +0000
@@ -14,7 +14,8 @@
   cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B
 
 
-exec : {I O : Set} {{_ : DataSegment I}} {{_ : DataSegment O}} -> CodeSegment I O -> Context -> Context
+exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} {{_ : DataSegment I}} {{_ : DataSegment O}}
+     -> CodeSegment I O -> Context -> Context
 exec {l} {{i}} {{o}}  (cs b) c = set o c (b (get i c))