[Agda] Question on the Agda tutorial
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?
More information about the Agda