Где находится _≡⟨_⟩_ стандартная библиотека Agda?

Question

Я читаю такой кусок кода в plfa.

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

, но _≡⟨_⟩_ отсутствует в PropositionalEquality

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

Я нахожу его только в Function.Related и Relation.Binary.HeterogeneousEquality. Что происходит?

Answer 1

_≡⟨_⟩_ является синтаксической нотацией для step-≡, как вы можете видеть в Relation.Binary.PropositionalEquality.Core.

Так что если вы хотите контролировать то, что вы импортируете, вам нужно обратиться вместо step-≡.