[Agda] Again, a question on records

[David Leduc]

Hugo Herbelin has explained this feature on the Coq mailing list.
I'd love to have this in Agda because it allows for nice notations.

http://permalink.gmane.org/gmane.science.mathematics.logic.coq.club/5284

On Tue, Sep 21, 2010 at 7:19 PM, Nils Anders Danielsson
<nad at cs.nott.ac.uk> wrote:
> On 2010-09-19 22:41, Dan Doel wrote:
>>
>> I'm not sure how Coq does it, either.
>
> For some reason the Coq unifier sometimes chooses a solution even if it
> is not unique.
>
> --
> /NAD
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>