[Agda] Question on the Agda tutorial

david rush kumoyuki at gmail.com
Wed Jul 10 23:03:36 CEST 2013


Hi y'all -

I've started working through the Agda tutorial in order to try and eliminate 
gaps in what I think I understand while hacking up a framework for numerical 
computation, and I ran across this question:

    Give an isomorphic definition of Maybe A with the help of _⊎_ and ⊤

And for the life of me I can't figure it out. Either the question is wrong or 
I've seriously missed something, because it seems to me that it would be easy 
to formulate a type isomorphic to Maybe A with the help of _⊎_ and ⊥.

Can someone tell me what I am missing, if anything?

TIA
- d



More information about the Agda mailing list