Sure. Coq is very similar to Haskell or OCaml. A function like that is defined in Coq.Arith.EqNat. It's called beq_nat
.
Boolean equality over natural numbers in Coq
-
29-09-2022 - |
Вопрос
Is it possible to compare two natural numbers, x and y, in Coq, and have the equality be returned as a boolean value? Ideally I would like to be able to do something like:
Variable x : nat.
Variable y : nat.
if bool_eq x y
then ...
else ...
Thanks in advance!
Решение
Не связан с StackOverflow