CODEWITHSUNDEEP
coq
Larry Lee
Larry Lee

Reputation: 189

Boolean equality over natural numbers in Coq

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!

Upvotes: 1

Views: 1357

Answers (1)

user1861759
user1861759

Reputation:

Sure. Coq is very similar to Haskell or OCaml. A function like that is defined in Coq.Arith.EqNat. It's called beq_nat.

Upvotes: 3

Related Questions