Zulip Chat Archive

Stream: new members

Topic: try this

Julian Berman (Jan 16 2021 at 21:58):

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 (Jan 16 2021 at 22:00):

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 (Jan 16 2021 at 22:01):

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

Julian Berman (Jan 16 2021 at 22:02):

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

Alex J. Best (Jan 16 2021 at 22:02):

Try this is jsut a trace message though

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

Julian Berman (Jan 16 2021 at 22:02):

Ah fantastic, thank you!

Last updated: Dec 20 2023 at 11:08 UTC