[Agda] wishlist/some help wanted

Nils Anders Danielsson nils.anders.danielsson at gmail.com
Mon Apr 28 15:24:35 CEST 2008


On Mon, Apr 28, 2008 at 1:22 AM, Tristan Wibberley
<tristan at wibberley.org> wrote:
>
>  For example, boolean or: a proof object of "(a || b) istrue" is also a
>  proof object of "(b || a) istrue".

Only in the case when the types are definitionally equal, i.e. only
when both a and b are constructors, not in general.

-- 
/NAD


More information about the Agda mailing list