agda - _≡⟨_⟩_ 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.Relatedand中找到它Relation.Binary.HeterogeneousEquality。怎么了？

标签： agda

Answer 1