I'm trying to create a Hint Rewrite database for a matrix library I've written. However when I write
Hint Rewrite kron_1_r : M_db
I get the following error:
Cannot infer the implicit parameter m of kron_1_r whose type is "nat".
kron_1_r has the type forall {m n : nat} (A : Matrix m n), A ⊗ Id 1 = A, so m and n should be inferred based on the context when autorewrite is called. I'm not sure why it wants a parameter here, or how to tell it to hold off.