From b6756fdc08a9dc67c08849154066ba1f6612ab28 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 23 Dec 2024 20:05:41 -0800 Subject: [PATCH] chore: missing `set_option grind.debug true` --- tests/lean/run/grind_canon_insts.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/lean/run/grind_canon_insts.lean b/tests/lean/run/grind_canon_insts.lean index 59b5b481f48b..ddbadb62f5e9 100644 --- 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)