[Agda] Problem with inductively defined type having (simulated) partial constructors

[Ulf Norell]

On Fri, Apr 18, 2008 at 1:35 AM, Tristan Wibberley <tristan at wibberley.org>
wrote:

>
> > >  proof1 {allzeros} {allzeros} p q = record {}
>
> record {} is what I was missing from my knowledge. I realised after I
> sent that email that I shouldn't be giving Top : Set but rather
> something that is a proof object of Top.
>

 Actually since there is a single unique inhabitant of Top the type checker
can figure out which one you want and you can simply write _, by the same
magic that allows elements of Top to be left implicit.


/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080418/47a85d40/attachment.html