Mercurial > hg > Members > atton > agda-proofs
changeset 73:a5cac9483f91
Cleanup sample
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 01 Feb 2017 05:27:05 +0000 |
| parents | dc8f140e299d |
| children | f1ab418bc37f |
| files | cbc/atton-master-sample.agda |
| diffstat | 1 files changed, 4 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/cbc/atton-master-sample.agda Wed Feb 01 05:05:35 2017 +0000 +++ b/cbc/atton-master-sample.agda Wed Feb 01 05:27:05 2017 +0000 @@ -33,14 +33,14 @@ _ = record { set = (\c d -> record c {c = (ds1.c d)}) ; get = (\c -> record { c = (Context.c c)})} -cs2 : {{_ : DataSegment ds1}} -> CodeSegment ds1 ds1 -cs2 {{d}} = cs {{d}}{{d}} id +cs2 : CodeSegment ds1 ds1 +cs2 = cs id cs1 : CodeSegment ds1 ds1 cs1 = cs (\d -> goto cs2 d) -cs0 : {{_ : DataSegment ds0}} {{_ : DataSegment ds1}} -> CodeSegment ds0 ds1 -cs0 {{d0}}{{d1}} = cs {{d0}}{{d1}} (\d -> goto {{d1}} {{d1}} cs1 (record {c = (ds0.a d) + (ds0.b d)})) +cs0 : CodeSegment ds0 ds1 +cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) main : ds1 main = goto cs0 (record {a = 100 ; b = 50})