Questions about grind

Stream: CSLib

[Ching-Tsun Chou]

I find grind rather hard to understand. I moved the following code:

@[scoped grind =]
def mtr (DA : DA State Symbol) (s : State) (xs : List Symbol) := xs.foldl DA.tr s

@[simp, scoped grind =]
theorem mtr_nil_eq {DA : DA State Symbol} {s : State} : DA.mtr s [] = s := rfl

from DFA.lean to DA.lean, because I want to use them in general constructions (such as product) about DA, not just about DFA (which extends DA). This move breaks quite a few grinds in various proofs about DFA and I had to give [DA.mtr] explicitly to those grinds to fix them. Why?

More generally, how should one proceed when grind fails? I find its error messages rather mysterious.

[Chris Henson]

Based on your description, my guess would be that you are just missing an open scoped DA after changing what namespaces these are in.

[Ching-Tsun Chou]

You are right! Thanks!