This is an experiment concerned with the way operators like + or ∘ are overloaded with instance arguments.
Currently, given e.g. A : AbGroup ℓ this is done by
open AbGroupStr ⦃...⦄
instance
_ = snd A
The idea is to gain better notation with more flexibility and overloading by separating the notation from the data structures (just look at the changes). Here are a couple of things that would be nice to have:
Use operators with the same name from different structures at the same time, for example _+_ from Semiring and CommRing.
Choose notation independent of the definition of a structure. For example, a CommMonoid used multiplicative notation in its definition, but one might want to use + in some contexts.
Have more readable output from agda. Currently, goals are sometimes written as something like AbGroupStr._+_ _ x y instead of x + y. I think that shouldn't happen if _+_ is defined on top level with an instance argument.
It is unclear to me, if this is a good idea performance-wise.
This is an experiment concerned with the way operators like
+or∘are overloaded with instance arguments. Currently, given e.g.A : AbGroup ℓthis is done byThe idea is to gain better notation with more flexibility and overloading by separating the notation from the data structures (just look at the changes). Here are a couple of things that would be nice to have:
_+_fromSemiringandCommRing.+in some contexts.AbGroupStr._+_ _ x yinstead ofx + y. I think that shouldn't happen if_+_is defined on top level with an instance argument.It is unclear to me, if this is a good idea performance-wise.