[Agda] Absurd question
m.escardo at cs.bham.ac.uk
Fri May 24 21:53:24 CEST 2013
On 24/05/13 18:33, Martin Escardo wrote:
> On 24/05/13 18:02, Andrea Vezzosi wrote:
>> The crucial point is that (\()) is not equal to (\()),
> Fair enough, an absurd question deserves an absurd answer.
(Of course, this was an irresistible joke.)
The "crucial point" allowed me to streamline, as I wanted, my proof.
Before I was fighting blindly against Agda without knowing what was
wrong, but now, knowing what the problem is, I could write a nicer
version of the proof.
Andreas (Abel) proposed a ticket to let \() be the same as \(), as it
should. My streamlined version of the proof wouldn't benefit from that.
But this equality would have saved several hours of my fruitless
attempts, and so I think this ticket is important (everybody often
writes an ugly proof first, and a number of us try to make it look
prettier after success.)
Very many thanks to those who made me understand the problem.
More information about the Agda