[Agda] Again, a question on records

[Andreas Abel]

Thanks for the pointer to Hugo's explanation!

I think this not unrelated to the "Pie in the Sky" discussion.   
Basically, we want some smart but perspicuous search for sensible  
resolution of hidden arguments...

However, I think in this case (records for mathematical structures)  
you could also work with the Agda module system. You can open a record  
like a module and work with the fields directly, so you have "carrier"  
and "op" already instantiated to a certain instance t of T.

On Sep 25, 2010, at 3:58 PM, David Leduc wrote:
> 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.

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/