chore: missing set_option grind.debug true

leanprover · Dec 24, 2024 · b6756fd · b6756fd
1 parent 35d4d65
commit b6756fd
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/tests/lean/run/grind_canon_insts.lean b/tests/lean/run/grind_canon_insts.lean
@@ -7,6 +7,8 @@ elab "grind_test" : tactic => withMainContext do
     let nodes ← filterENodes fun e => return e.self.isAppOf ``HMul.hMul
     logInfo (nodes.toList.map (·.self))
 
+set_option grind.debug true
+
 class Semigroup (α : Type u) extends Mul α where
   mul_assoc (a b c : α) : a * b * c = a * (b * c)