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