HiI have a definition of the formT::= T_1 | T_2 | T_3I can use T_1+T_2+T_3 with explicit inl, inr but it isn't a good solution. What can I do else? Pavel -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.chalmers.se/pipermail/agda/attachments/20160303/99950218/attachment.html