[Agda] A proof of the irrationality of the square root in Agda

[IKEGAMI Daisuke]

2011/11/11 Nils Anders Danielsson <nad at chalmers.se>:
> On 2011-11-07 07:03, IKEGAMI Daisuke wrote:
>>
>> Nils, I'm pleased to add your name to the title of the talk, as
>>   "joint work with Nils Anders Danielsson".
>>   Thank every contributers of Agda and especially you.
>
> Thanks. However, "joint work" sounds a bit strange, given that I don't
> really know what you're working on; an ordinary acknowledgement seems
> more suitable.
>
> --
> /NAD

I apologize to you for my rudeness. I didn't understand the meaning
of 'joint work'. The title of my talk will be changed soon.

Almost all proofs on the work is based on the Agda standard library.
I want to thank to the authors. Arseniy and Nils help me a lot to prove
important part (yet not finished, though).
In the talk, I will explain the contribution appropriately.

Sincerely,
Ike