_??_?_ 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-? 。