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

[Andreas Abel]

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

if

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

And so on...

Cheers,
Andreas


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
http://www2.tcs.ifi.lmu.de/~abel/