agda - _≡⟨_⟩_ Agda 标准库在哪里？

Question

我在plfa读到这样一段代码。

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

但是 _≡⟨_⟩_不是命题平等

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-≡反而。