Where is _≡⟨_⟩_ Agda standard lib?

Question

I read such a piece of code in plfa.

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

but _≡⟨_⟩_ is not in PropositionalEquality

The module Eq.≡-Reasoning doesn't export the following: _≡⟨_⟩_
when scope checking the declaration
  open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)

I only find it in Function.Related and Relation.Binary.HeterogeneousEquality. What is happening?

Ninepins

Answer 1

_≡⟨_⟩_ is a syntax notation for step-≡ as you can see in Relation.Binary.PropositionalEquality.Core.

So if you want to control what you are importing, you need to refer to step-≡ instead.

Flasket

Sorry, I still don’t understand... I just want to import _≡⟨_⟩_, what import statement should I write? – Ninepins

replace _≡⟨_⟩_ with step-≡ in your import statement from your question. – Brassbound

open ≡-Reasoning – Hydromancy