我多次遇到这个问题:我在 Coq 中有一个证明状态,其中包括相同等式两边的匹配项。
是否有一种标准方法可以将多个匹配项重写为一个匹配项?
例如。
match expression_evaling_to_Z with
Zarith.Z0 => something
Zartih.Pos _ => something_else
Zarith.Neg _ => something_else
end = yet_another_thing.
如果我破坏expresion_evaling_to_Z
我会得到两个相同的目标。我想找到一种方法来实现其中一个目标。