coq中的多态等式

Question

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

3==5

和

"hello" == "hello"

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

谢谢。

Answer 1

Ssreflect具有eqType类，它正是您需要的：

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.

Check (3 == 5).

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