Coq Tutorialeq_nat is recursively defined to test equality of two natural numbers n and m by pattern matching on their constructions. It returns true if both are 0, or if their successors S n' and S m' are recursively equal; otherwise it returns false. Evaluating eq_nat 3 3 returns true since 3 is constructed by applying S twice to 0, and both arguments have the same construction.Read less
