Mercurial > hg > Members > atton > agda-proofs

changeset 53:6af88ee5c4ca

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prune level
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 10 Jan 2017 09:07:07 +0000
parents 4880184e4ab5
children fa95e3070138
files cbc/stack-subtype.agda cbc/subtype.agda
diffstat 2 files changed, 9 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/cbc/stack-subtype.agda	Tue Jan 10 09:04:55 2017 +0000
+++ b/cbc/stack-subtype.agda	Tue Jan 10 09:07:07 2017 +0000
@@ -30,8 +30,8 @@
 open import subtype Context
 
 instance
-  yo : DataSegment Context
-  yo = record {get = (\x -> x) ; set = (\_ c -> c)}
+  ContextIsDataSegment : DataSegment Context
+  ContextIsDataSegment = record {get = (\x -> x) ; set = (\_ c -> c)}
 
 
 
--- a/cbc/subtype.agda	Tue Jan 10 09:04:55 2017 +0000
+++ b/cbc/subtype.agda	Tue Jan 10 09:07:07 2017 +0000
@@ -1,28 +1,28 @@
 open import Level
 open import Relation.Binary.PropositionalEquality
 
-module subtype {l : Level} (Context : Set l) where
+module subtype (Context : Set) where
 
 
-record DataSegment {ll : Level} (A : Set ll) : Set (l ⊔ ll) where
+record DataSegment (A : Set) : Set where
   field
     get : Context -> A
     set : Context -> A -> Context
 open DataSegment
 
-data CodeSegment {ll : Level} (A B : Set ll) : Set (l ⊔ ll) where
+data CodeSegment (A B : Set) : Set where
   cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B
 
 
-exec : {I O : Set l} {{_ : DataSegment I}} {{_ : DataSegment O}} -> CodeSegment I O -> Context -> Context
+exec : {I O : Set} {{_ : DataSegment I}} {{_ : DataSegment O}} -> CodeSegment I O -> Context -> Context
 exec {l} {{i}} {{o}}  (cs b) c = set o c (b (get i c))
 
 
-comp : {con : Context} -> {A B C D : Set l} {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
+comp : {con : Context} -> {A B C D : Set} {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
        -> (C -> D) -> (A -> B) -> A -> D
 comp {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x)))
 
-csComp : {con : Context} {A B C D : Set l}
+csComp : {con : Context} {A B C D : Set}
          {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
        -> CodeSegment C D -> CodeSegment A B -> CodeSegment A D
 csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} (cs g) (cs f)
@@ -30,7 +30,7 @@
 
 
 
-comp-associative : {A B C D E F : Set l} {con : Context}
+comp-associative : {A B C D E F : Set} {con : Context}
                    {{da : DataSegment A}} {{db : DataSegment B}} {{dc : DataSegment C}}
                    {{dd : DataSegment D}} {{de : DataSegment E}} {{df : DataSegment F}}
                    -> (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F)