[Agda] error in plfa exercise

[Philip Wadler]

Which version of Agda are you using? The book is currently released for
Agda 2.6.0.1, Agda stdlib 1.1. We will upgrade soon. Go well, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/



On Wed, 15 Apr 2020 at 12:14, Michel Levy <michel.levy.imag at free.fr> wrote:

> When I try to reproduce the currying proof, I get the following error
> Expected non-abstract record type, found
> (.A → .B → .C) ≃ .A x .B → .C
> when checking that the expression
> record
> { to = λ { f → λ { < x , y > → (f x) y } }
> from = λ { g → λ { x y → g < x , y > } }
> ; from∘to = λ { f → refl }
> ; to∘from = λ { g → extensionality λ { < x , y > → refl } }
> }
> has type (.A → .B → .C) ≃ .A x .B → .C
>
> Where does this error come from, from my too old version of agda?
>
> --
> courriel : michel.levy.imag at free.fr
> mobile : 06 59 13 42 53
> web : michel.levy.imag.free.fr
> _______________________________________________
> 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/20200415/751f9489/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200415/751f9489/attachment.ksh>