[Agda] Infix-notation and TDNR

[a.j.rouvoet]

You can locally declare two modules with the same name as the record 
instances
to accomplish what you want; e.g.:

   record Functor (ℂ : Category) (𝔻 : Category) : Set where
     module ℂ = Category ℂ
     module 𝔻 = Category 𝔻
     field
       distrib : {A B C : ℂ.Object} {g : ℂ.Arrow B C} {f : ℂ.Arrow A B} 
→ func→ (g ℂ.⊕ f) ≡ (func→ g) 𝔻.⊕ (func→ f)


Regards,

Arjen


On 01/22/2018 12:04 PM, Frederik Hanghøj Iversen wrote:
> I just discovered a new feature in Agda. I don't know what's it's 
> called (haven't been able to find any documentation on it) so let me 
> just name it Type-Directed Name-space Resolution (TDNR).
>
> The feature I'm talking about it the one that e.g lets you project a 
> field `Object` of a term `ℂ` of type `Category` that has this field 
> like so:
>
>      ℂ .Object
>
> What I would like to do is use the infix version of this. So for 
> instance for a field `_⊕_` I would like to express the distributive 
> properties of functors like so:
>
>     func→ (g (ℂ .⊕) f) ≡ func→ g (𝔻 .⊕) func→ f
>
> Or perhaps even with backticks (as in Haskell) like so:
>
>     func→ (g `ℂ .⊕` f) ≡ func→ g `𝔻 .⊕` func→ f
>
> In stead I am left with writing it like so:
>
>     func→ (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (func→ g) (func→ f)
>
> Which is not so readable.
>
> I've attached an MWE.
>
> -- 
> Regards
> /Frederik Hanghøj Iversen/
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180122/9421afe5/attachment.html>