try this

Stream: new members

[Julian Berman]

I'm trying to get Lean to give me a "Try this: ..." message and hopefully one without needing something from mathlib. I found exactly one instance in Lean core, which looks like in something called trace_lemmas, a parameter to simp (https://github.com/leanprover-community/lean/blob/ec45183aa01354e8e2c273cf762cf53ead277fe4/library/init/meta/interactive.lean#L1296) -- but it looks like that parameter maybe isn't exposed externally (anymore?) because e.g. example (n : ℕ) : n = n := by simp {trace_lemmas := tt} tells me 'trace_lemmas' is not a field of structure 'tactic.simp_config_ext'

Is there anything I'm doing wrong there, or am I correct that it's being hidden (I guess because there are better other things that exist now like squeeze_simp?)

Or, any suggestion on how to get that kind of message another way, I guess what I see there with trace() is a way I can emit such a message myself if I try writing some meta thing?

[Bryan Gin-ge Chen]

I think that what you found in core was just recently added by @Johan Commelin and it will replace squeeze_simp whenever Lean 3.25.0 is released and mathlib is upgraded.

[Julian Berman]

Oh, indeed, it's 8 days old, that'll teach me not to git blame before asking.

[Julian Berman]

So I guess the actual answer may be that I'm on 3.24

[Alex J. Best]

Try this is jsut a trace message though

example : ∃ n, n =2 :=
begin
  (do tactic.trace "Try this: use 2"),
end

[Julian Berman]

Ah fantastic, thank you!