Mercurial > hg > Members > atton > agda-proofs

comparison cbc/subtype.agda @ 71:614997a2e21c

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