[Agda] How to validate eta-reduction in equational reasoning proofs?

[David Banas]

Thanks, Oleg!
Is this correct?:

55 record _×_ (A : Set) (B : Set) : Set where
56   field
57     fst : A
58     snd : B
59     
60 _,_ : ∀ {A B : Set} A → B → (A × B)
61 x , y = record {fst = x; snd = y}

It seems to work, in general, but is giving me the following error, re: my Functor instance:

###.agda:112,3-36
Could not parse the left-hand side
fmap ⦃ ProductFunctor ⦄ f (x , y)
Operators used in the grammar:
  , (infix operator, level 20) [_,_ (###.agda:60,1-4)]
when scope checking the left-hand side
fmap ⦃ ProductFunctor ⦄ f (x , y) in the definition of
ProductFunctor

For reference, here is that Functor instance:

110 instance
111   ProductFunctor : ∀ {A : Set} → Functor (_× A)
112   fmap {{ProductFunctor}} f (x , y) = (f x , y)

Thanks,
-db


> On Jan 14, 2021, at 12:08 PM, Oleg Grenrus <oleg.grenrus at iki.fi> wrote:
> 
> You need to define the type as a record.
> 
> See
> https://agda.readthedocs.io/en/v2.6.1/language/record-types.html#eta-expansion <https://agda.readthedocs.io/en/v2.6.1/language/record-types.html#eta-expansion>
> 
> - Oleg

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210114/3cefbaae/attachment.html>