Skip to content

Commit f746e3a

Browse files
committed
chore: fix
1 parent bac6cab commit f746e3a

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

tests/lean/run/try_induction.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -130,14 +130,14 @@ theorem hyperoperation_recursion (n m k : ℕ) :
130130
/--
131131
info: Try these:
132132
[apply] (induction k) <;> grind
133-
[apply] (induction k) <;> grind only [hyperoperation, = add_zero, = add_succ, = hyperoperation_zero]
133+
[apply] (induction k) <;> grind only [hyperoperation, = add_zero, = add_succ]
134134
[apply] ·
135135
induction k
136136
· grind => instantiate only [hyperoperation, = add_zero]
137137
·
138138
grind =>
139139
instantiate only [hyperoperation, = add_succ]
140-
instantiate only [= hyperoperation_zero]
140+
instantiate only [hyperoperation]
141141
-/
142142
#guard_msgs in
143143
@[grind =]

0 commit comments

Comments
 (0)