[Agda] _≡⟨_⟩_ operator

[Philip Wadler]

Philippe,

Every chapter of PLFA has a section at the end telling you where to find
relevant definitions in the Standard Library. Here's the one for Equality:
  https://plfa.github.io/Equality/#standard-library
As mentioned by Alexander, you need to use the right version of the library.

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 Mon, 4 May 2020 at 13:28, Philippe de Rochambeau <phiroc at free.fr> wrote:

> Hello,
>
> The https://plfa.github.io/Induction Page mentions the _≡⟨_⟩_ operator,
> which I couldn’t find on
> https://agda.github.io/agda-stdlib/Relation.Binary.PropositionalEquality.Core.html
>
> Does it have an existing equivalent in the Standard Library?
>
> Cheers,
>
> Philippe
>
> PS My apologies if this question has already been asked on this list
> _______________________________________________
> 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/20200504/44a4f10e/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200504/44a4f10e/attachment.ksh>