Coq: Boolean Сравнение целых чисел

Question

Естественные числа (nat) в coq имеют функцию beq_nat, существует ли подобная функция для целых чисел Z (в ZArith)?

И как в будущем, как я могу найти ответ на такие вопросы, не спрашивая о Stackoverflow?

Answer 1

В стандартной библиотеке есть функция Z.eqb. Обязательно импортируйте модуль ZArith tp.

К сожалению, я не знаю, какие ресурсы можно найти, кроме просмотра документации standard library ...