如何在 if 语句中使用与有理数的比较？
if 1 = 2 then 1 else 2
1 = 2 当然是 Prop 而不是 bool。
最佳答案
我不明白 dfan 的回答与问题有什么关系...
当然，1 = 2 是一个Prop，它是1 等于2 的陈述。希望你没有这个陈述的证明。 ..
你想要的是一个函数，给定两个自然数 1 和 2，如果它们相等则返回 true，并且 false 如果不是。
Coq.Arith.EqNat 库为您提供了这样一个函数，名为 beq_nat。
事实上，您可能想要更好的东西，一个返回相等证明或差异证明的函数:
(* In Coq.Arith.Peano_dec *)
Theorem eq_nat_dec : forall n m, {n = m} + {n <> m}.
(* ^ a proof that n = m
^ or a proof that n <> m *)
if 被重载来处理这些事情，所以你甚至可以写:
if eq_nat_dec 2 3 then ... else ...
关于boolean - Coq 中的 prop 和 bool，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/22798759/