[Agda] _≡⟨_⟩_ operator

[Alexander Ben Nasrallah]

Hi Philippe,

On Mon, May 04, 2020 at 06:27:58PM +0200, Philippe de Rochambeau wrote:
> 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?

You have to be careful about the stdlib version. plfa uses v1.2.
The current version is v1.3.

Assuming you installed Agda stdlib v1.3, did you try?

	import Relation.Binary.PropositionalEquality as Eq
	open Eq using (_≡_; refl; cong; sym)
	open Eq.≡-Reasoning

Note the missing using statement compared to the code in plfa. With
stdlib v1.3 you can’t use `using` or `hide` with _≡⟨⟩_. They changed the
definition
https://github.com/agda/agda-stdlib/blob/v1.3/CHANGELOG.md#changes-to-how-equational-reasoning-is-implemented

I don’t unterstand the details why it doesn’t work anymore, I just know
how to deal with it ^^

Hope that helps.
Alex

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200504/e6211708/attachment.sig>