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

[David Banas]

Ah, thanks!

With that help, my code is compiling, but I'm getting some unsolved
constraint errors:

  _82 (C→A⇒D = (λ C₁ → ƛ (λ A₁ → C×A→D (C₁ , A₁)))) = Set
  _83 (C→A⇒D = (λ C₁ → ƛ (λ A₁ → C×A→D (C₁ , A₁)))) = C × A

I don't really understand them.
Is there something in the Agda docs on this that you could point me to?

Thanks,
-db


On Thu, Jan 14, 2021 at 2:29 PM Oleg Grenrus <oleg.grenrus at iki.fi> wrote:

> See
>
> https://agda.readthedocs.io/en/v2.6.1/language/record-types.html#example-the-pair-type-constructor
> ,
> specifically the last paragraphs about `constructor` keyword.
>
> - Oleg
>
> On 15.1.2021 0.21, David Banas wrote:
> > 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
> >> <mailto: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
> >>
> >> - Oleg
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210114/e2c6b882/attachment.html>