[Agda] Infix-notation and TDNR

[Sandro Stucki]

The feature is called "postfix projections", BTW.

https://github.com/agda/agda/issues/1963

Cheers
/Sandro


On Jan 22, 2018 1:07 PM, "a.j.rouvoet" <a.j.rouvoet at gmail.com> wrote:

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 listAgda at lists.chalmers.sehttps://lists.chalmers.se/mailman/listinfo/agda



_______________________________________________
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/11eda0d8/attachment.html>