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

[Dan Doel]

On Mon, May 14, 2012 at 2:51 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> What is your opinion on this from your experience with Agda?  How would you
> fixops expect to work?  Should records behave differently than modules?

I have one example for consideration. When defining functors in the
past, I've written:

    record Functor (C D : Category) ... where
      field
        _•_ : Category.Obj C -> Category.Obj D
        ...

    open Functor using (_•_)

Now, if I have a functor F, I can write F • A. But, this is only due
to the behavior in your message. I don't have a module-only example
off the top of my head, though.

-- Dan