Mercurial > hg > Members > atton > agda-proofs

comparison cbc/subtype.agda @ 74:f1ab418bc37f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Cleanup sample
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Wed, 01 Feb 2017 05:28:30 +0000
parents 614997a2e21c
children
comparison
equal deleted inserted replaced
73:a5cac9483f91 74:f1ab418bc37f
11 open DataSegment 11 open DataSegment
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 goto : {l1 l2 : Level} {I : Set l1} {O : Set l2} {{_ : DataSegment I}} {{_ : DataSegment O}} 16 goto : {l1 l2 : Level} {I : Set l1} {O : Set l2} -> CodeSegment I O -> I -> O
17 -> CodeSegment I O -> I -> O
18 goto (cs b) i = b i 17 goto (cs b) i = b i
19 18
20 exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} {{_ : DataSegment I}} {{_ : DataSegment O}} 19 exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} {{_ : DataSegment I}} {{_ : DataSegment O}}
21 -> CodeSegment I O -> Context -> Context 20 -> CodeSegment I O -> Context -> Context
22 exec {l} {{i}} {{o}} (cs b) c = set o c (b (get i c)) 21 exec {l} {{i}} {{o}} (cs b) c = set o c (b (get i c))