[Agda] [agda2] how to programming the basic

[Mandy Martino]

SGkgU2VyZ2VpLA0KDQoxLg0KaSBkZWZpbmVkICBtdXR1YWwgIGJsb2NrICBidXQgIGNhbiBub3Qg
cGFyc2UuDQoNCkNvdWxkIG5vdCBwYXJzZSB0aGUgYXBwbGljYXRpb24gbSArMiBuICoyIG0NCndo
ZW4gc2NvcGUgY2hlY2tpbmcgbSArMiBuICoyIG0NCg0KMi4gd2hlbiBjb21tZW50IGFib3ZlIGVy
cm9yIGNvZGUgLCBhbmQgY29udGludWUgdG8gcnVuLCBpdCBoYXMgIGVycm9yIGF0ICBpZjJfdGhl
bjJfZWxzZTJfIEJvb2wyIHRydWUgKHB1dFN0ckxuICJpdCBpcyB0cnVlIikgKHB1dFN0ckxuICJp
dCBpcyBlbHNlIGNhc2UiKQ0KVHlwZSBtaXNtYXRjaA0Kd2hlbiBjaGVja2luZyB0aGF0IHRoZSBw
YXR0ZXJuIHRydWUgaGFzIHR5cGUgU2V0DQoNCm9wZW4gaW1wb3J0IFByZWx1ZGUNCg0KZGF0YSBC
b29sMiA6IFNldCB3aGVyZQ0KIHRydWUgOiBCb29sMg0KIGZhbHNlIDogQm9vbDINCg0Kbm90MiA6
IEJvb2wyIC0+IEJvb2wyDQpub3QyIHRydWUgPSBmYWxzZQ0Kbm90MiBmYWxzZSA9IHRydWUNCg0K
aWRlbnRpdHkyIDogKEEgOiBTZXQpIC0+IEEgLT4gQQ0KaWRlbnRpdHkyIEEgeCA9IHgNCg0KZGF0
YSBOYXQyIDogU2V0IHdoZXJlDQogemVybzIgOiBOYXQyDQogc3VjIDogTmF0MiAtPiBOYXQyDQoN
Cm11dHVhbA0KIF8rMl8gOiBOYXQyIC0+IE5hdDIgLT4gTmF0Mg0KIHplcm8yICsyIG0gPSB6ZXJv
Mg0KIHN1YyBuICsyIG0gPSBzdWMgKG4gKzIgbSkNCg0KIF8qMl8gOiBOYXQyIC0+IE5hdDIgLT4g
TmF0Mg0KIHplcm8yICoyIG0gPSB6ZXJvMg0KIHN1YyBuICoyIG0gPSBtICsyIG4gKjIgbQ0KDQpf
b3IyXyA6IEJvb2wyIC0+IEJvb2wyIC0+IEJvb2wyDQpmYWxzZSBvcjIgeCA9IHgNCnRydWUgb3Iy
IF8gPSB0cnVlDQoNCmlmMl90aGVuMl9lbHNlMl8gOiAoQSA6IFNldCkgLT4gQm9vbDIgLT4gQSAt
PiBBIC0+IEENCmlmMiB0cnVlIHRoZW4yIHggZWxzZTIgeSA9IHgNCmlmMiBmYWxzZSB0aGVuMiB4
IGVsc2UyIHkgPSB5DQoNCm1haW4gPSANCiBpZjJfdGhlbjJfZWxzZTJfIEJvb2wyIHRydWUgKHB1
dFN0ckxuICJpdCBpcyB0cnVlIikgKHB1dFN0ckxuICJpdCBpcyBlbHNlIGNhc2UiKQ0KIHB1dFN0
ckxuICJIZWxsbyBXb3JsZCINCg0KUmVnYXJkcywNCg0KTWFydGluIA0KDQpfX19fX19fX19fX19f
X19fX19fX19fX19fX19fX19fX19fX19fX19fDQqxSKXzqsw6IFNlcmdlaSBNZXNodmVsaWFuaSA8
bWVjaHZlbEBib3Rpay5ydT4NCrFIpfOk6bTBOiAyMDE2pn4xpOsyNKTpIDIyOjQ3DQqmrKXzqsw6
IE1hbmR5IE1hcnRpbm8NCrDGpbs6IGFnZGFAbGlzdHMuY2hhbG1lcnMuc2UNCqVEpq46IFJlOiBb
QWdkYV0gW2FnZGEyXSBob3cgdG8gcHJvZ3JhbW1pbmcgdGhlIGJhc2ljDQoNCk9uIFN1biwgMjAx
Ni0wMS0yNCBhdCAxMjo1MiArMDAwMCwgTWFuZHkgTWFydGlubyB3cm90ZToNCj4gSSB1c2UgdGhl
IHNjcmlwdCBpbiB0dXRvcmlhbCBhbmQganVzdCBhcHBlbmQgMg0KPg0KPg0KPiBEbyBpdCBoYXZl
IHByaW9yaXR5IG9mIGRlZmluaW5nIHdoaWNoIGZpcnN0Pw0KPg0KPg0KPiBCZWNhdXNlICsyIGFu
ZCAqMiAgZGVwZW5kIG9uIGVhY2ggb3RoZXINCj4NCj4NCj4gSSBndWVzcyB0aGUgb3JpZ2luYWwg
c2NyaXB0IGluIHR1dG9yaWFsIGRvIG5vdCBoYXZlIHRoaXMgcHJvYmxlbS4NCg0KDQoqMiAgdXNl
cyAgKzIsICBhbmQgKzIgbmVlZHMgbm90IHRvIHVzZSAqMi4NCkhlbmNlICsyIG5lZWRzIHRvIGJl
IGRlZmluZWQgZWFybGllciB0aGFuICoyLg0KDQpJZiBmIHVzZXMgZywgYW5kIGcgdXNlcyBmLCB0
aGVuIHRoZXkgbmVlZCB0byBiZSBkZWZpbmVkIGluIHRoZSBgbXV0dWFsJw0KYmxvY2s6DQogIG11
dHVhbA0KICAgIGYgOiAuLi4NCiAgICBmID0gLi4uIGcgLi4uDQoNCiAgICBnIDogLi4uDQogICAg
ZyA9IC4uLiBmIC4uLg0KDQpSZWdhcmRzLA0KDQotLS0tLS0NClNlcmdlaQ0KDQo+DQo+DQo+DQo+
DQo+DQoNCg==