Coq中的自然數的布爾相等

Question

是否可以比較Coq中的兩個自然數x和y，並將相等性作爲布爾值返回？理想情況下，我希望能夠做到這樣的事情：

Variable x : nat. 
Variable y : nat. 

if bool_eq x y 
    then ... 
    else ... 

在此先感謝！

Answer 1

當然。 Coq與Haskell或OCaml非常相似。像這樣的功能在Coq.Arith.EqNat中定義。它被稱爲beq_nat。