是否可以 remove/override 现有的强制转换？
Is it possible to remove/override an existing coercion?
我已经导入了一个定义强制转换的 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 尊重我的选择，至少在这个文件的本地？
如果能够在声明强制转换后显式地对其进行操作，那将是一个加分项，就像一个人如何能够操作提示数据库一样。有没有这样的命令？
使用 Coq 8.15，您可以导入除强制转换之外的所有内容：
Import -(coercions) ModuleName.
比照。 import categories.
的手册
我已经导入了一个定义强制转换的 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 尊重我的选择，至少在这个文件的本地？
如果能够在声明强制转换后显式地对其进行操作，那将是一个加分项，就像一个人如何能够操作提示数据库一样。有没有这样的命令？
使用 Coq 8.15，您可以导入除强制转换之外的所有内容：
Import -(coercions) ModuleName.
比照。 import categories.
的手册