[Agda] Poll: Mixfix and parametrized modules --- which behavior would you expect

Andreas Abel andreas.abel at ifi.lmu.de
Fri May 18 10:19:49 CEST 2012

Hi Benja,

giving hidden arguments to fixops is definitely a missing feature.

Can you put your proposal for supplying hidden arguments to fixops on 
the Agda issue tracker?

But I guess it must be worked out a bit, e.g. what is meant by

   x ~{A} y


   _~_ : {h : H}(x : X){i : I}(y : Y){j : J} -> Z

And so on...


On 14.05.12 10:39 AM, Benja Fallenstein wrote:
> I've recently grappled with non-inferrable implicit parameters to
> infix ops a couple of times. I'm wondering whether it would be worth
> it to allow
> x ~ {A} y
> to mean _~_ {A} x y; given the behavior of {}, could presumably also be written
> x ~{A} y
> This doesn't look all that weird to me if I think of {...} as a
> subscript, à la Epigram.
> Cheers,
> - Benja

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

More information about the Agda mailing list