[Agda] Re: Question on the Agda tutorial

[david rush]

Andrés Sicard-Ramírez <andres.sicard.ramirez at ...> writes:
> David Rush writes:
> > Can someone tell me what I am missing, if anything?

Thanks all, and especially to Wojtek Jedynak who mailed me privately and 
helped me realize that I was thinking in another language (*cough* Scheme) 
where there are multiple concepts that are vaguely similar to \bot but 
which, most definitely are not.

- d