我正在尝试为我编写的矩阵库创建一个提示重写数据库。但是当我写
Hint Rewrite kron_1_r : M_db
我收到以下错误：
Cannot infer the implicit parameter m of kron_1_r whose type is "nat".
kron_1_r具有 type forall {m n : nat} (A : Matrix m n), A ⊗ Id 1 = A，因此 m 和 n 应在调用 autorewrite 时根据上下文推断。我不确定为什么它需要一个参数，或者如何告诉它推迟。
您遇到了最大插入隐式参数和普通隐式参数之间的区别。不同之处在于，当您使用定义而不给出任何参数时，您在Hint Rewrite kron_1_r. 一种解决方案当然是使用@kron_1_r，它给出了没有任何隐式参数的标识符。
不幸的是，在创建定义时没有语法给它非最大插入的隐式参数；你只能使用{m : nat}. 相反，您需要Arguments kron_1_r [m n] _.在创建后使用kron_1_r来更改前两个参数的隐式行为（如上面的 Anton Trunov 所建议）。
使用它通常很有帮助About，它报告隐式参数的状态（你也可以得到这些Print，但是当你打印定理时你通常会得到太多的输出，因为证明项很大）。