diff --git a/test/LibrarySearch/basic.lean b/test/LibrarySearch/basic.lean index 656d3da768f53..cc0daa0fcbc69 100644 --- a/test/LibrarySearch/basic.lean +++ b/test/LibrarySearch/basic.lean @@ -19,7 +19,7 @@ set_option pp.unicode.fun true noncomputable section -/-- info: Try this: exact Nat.lt.base x -/ +/-- info: Try this: exact Nat.lt_add_one x -/ #guard_msgs in example (x : Nat) : x ≠ x.succ := ne_of_lt (by apply?)