Coq中的多态相等性

Question

3

我找不到一个标准库函数，它可以重载并返回布尔值（或sumbool或我可以进行计算的其他内容）。我希望能够这样做：

3==5

并且

"hello" == "hello"

不需要指定参数的类型。如果Coq没有这个相等类型的功能，我会非常惊讶的；能否告诉我在哪里找到它？我感觉这与ssreflect有些关联，但我无法弄清楚。

谢谢。

- push33n

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Arthur Azevedo De Amorim · Accepted Answer

Ssreflect拥有eqType类，该类恰好具备您所需要的功能：

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.

Check (3 == 5).

大多数标准类型在ssreflect中都定义了等式运算符。不幸的是，字符串并不是其中之一，但自己编写也不难。（Deriving库带有一个实例，但尚未标记为稳定版本。）