_≡⟨_⟩_ 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

正如您在Relation.Binary.PropositionalEquality.Core中看到的那样，_≡⟨_⟩_是step-≡的语法表示法。

因此，如果您希望控制要导入的内容，则需要改为引用step-≡。