[Agda] _≡⟨_⟩_ operator

[Philippe de Rochambeau]

Hi Alex,
commenting out Eq.≡-Reasoning’s using statement worked.
Many thanks.
Pleasant evening.
Philippe

module Induct where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning -- using (begin_; _≡⟨⟩_; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p =
  begin
    (zero + n) + p
  ≡⟨⟩
    n + p
  ≡⟨⟩
    zero + (n + p)
  ∎

+-assoc (suc m) n p =
  begin
    (suc m + n) + p
  ≡⟨⟩
    suc (m + n) + p
  ≡⟨⟩
    suc ((m + n) + p)
  ≡⟨ cong suc (+-assoc m n p) ⟩
    suc (m + (n + p))
  ≡⟨⟩
    suc m + (n + p)
  ∎




> Le 4 mai 2020 à 18:47, Alexander Ben Nasrallah <me at abn.sh> a écrit :
> 
> 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
> 
> _______________________________________________
> 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/dbec9e61/attachment.html>