typeclass - 重写子证明中的“未能合成类型类实例”

Question

下面的代码验证失败，并显示“无法为...合成类型类实例⊢ has_pow R R”。

这看起来很奇怪，因为我^在封闭范围内的相同类型上使用了相同的运算符 ()，并且没有问题！具有相同签名的第二个定理可以很好地进行类型检查。

为什么它只在重写内部失败？如何在不更改定理类型签名的情况下修复它？

import algebra.group_power

theorem pow_eq_zero_1 {R : Type} [domain R] {r : R} {n : ℕ} : r ^ (n + 1) = 0 → r = 0
:= begin
  rw (show r ^ (n + 1) = r ^ n * r,
      by { have rn := λ x : R, r ^ x,
           sorry, }),
  sorry,
end

theorem pow_eq_zero_2  {R : Type} [domain R] {r : R} {n : ℕ} : r ^ (n + 1) = 0 → r = 0
:= pow_eq_zero  -- it's in mathlib

标签： typeclasslean

Answer 1