Я импортировал модуль Coq, который определяет приведение, но он не соответствует моим потребностям.Есть ли способ удалить или (локально) переопределить его?
Если говорить точнее, скажем, модуль, который я импортировал, определяет приведение
Coercion bool_to_nat (b:bool) := match b with true => 1 | false => 0 end.
, но я хочуиспользуйте противоположное в моем коде
Local Coercion bool_to_nat' (b:bool) := match b with true => 0 | false => 1 end.
Coq выдает предупреждение Ambiguous paths: [bool_to_nat'] : bool >-> nat и просто игнорирует мое определение (может быть проверено Goal false + 1 = true. reflexivity. Qed. Можно ли убедить Coq уважать мойвыбор, по крайней мере локально в этом файле?
Было бы плюсом иметь возможность явно манипулировать приведениями после их объявления, например, как можно манипулировать базами данных подсказок. Существуют ли такие команды?