Search code examples
equalitycoqcoqide

How to check equality between two integers in Coq?

I'm trying to check the equality between two integers in Coq, but I get this error: "The term "first = second" has type "Prop" which is not a (co-)inductive type.". Is there any library in Coq that provides equality checking? Here is my code: 

Definition verify_eq (first : Z) (second : Z) : Z :=
   if first = second then 0 else 1.
Solution

  • You're in luck! In the same module where Z is defined (I'm assuming ZArith in the standard library), there's a term Z.eqb : Z -> Z -> bool that gives a a boolean test for integer equality (technically it's in the submodule Z — that's why there's a Z in the name).

    Require Import ZArith. (* I assume you already imported this, since you're using Z *)

Definition verify_eq (first : Z) (second : Z) : Z :=
   if Z.eqb first second then 0 else 1.