coq - coq中的多态相等

Question

我找不到标准库 == 函数，它被重载并返回布尔值（或 sumbool，或我可以计算的东西）。我希望能够做到

3==5

和

"hello" == "hello"

无需指定参数的类型。如果 Coq 没有平等类型的这个功能，我会感到惊讶。有人可以告诉我在哪里可以找到它吗？我觉得它与 ssreflect 有关，但我无法弄清楚。

谢谢。

Answer 1

Ssreflect 有这个eqType类，它有你需要的东西：

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.

Check (3 == 5).

大多数标准类型都有一个在 ssreflect 中定义的相等运算符。不幸的是，字符串不是其中之一，尽管自己卷起来并不难。（Deriving 库附带一个实例，但尚未标记为稳定。）