我想考虑 Coq 中实数的相等性。
但是 Coq.Reals.Reals. 中的 R 不是归纳类型，所以我不能定义像 Nat.eqb 这样的函数。
如何在 Coq 中定义实数相等？
最佳答案
实数在 Coq 中被公理化，它们的相等运算符也是如此:
Require Import Coq.Reals.Reals.
Check Req_EM_T.
(* forall r1 r2 : R, {r1 = r2} + {r1 <> r2} *)
{r1 = r2} + {r1 <> r2} type 是一个提供信息的 bool 值，可以为您提供两个实数是否相等的证明。
关于coq - 非归纳类型的类型相等，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/64303608/