Friends of `with_reducible`

Stream: lean4

[Heather Macbeth]

Is there something like with_reducible for other transparencies (in particular "all")?

Simple question, but I couldn't track down with_reducible in #docs4 to answer it for myself.

[Alex J. Best]

docs4#Lean.Parser.Tactic.withReducible (I guessed the name based on how these declarations are normally capitalized vs the tactic itself).
So looks like you want docs4#Lean.Parser.Tactic.withUnfoldingAll ?

[Kyle Miller]

In increasing order of what they allow to be unfolded, there's with_reducible, with_reducible_and_instances, (missing: with_default), with_unfolding_all.

When metaprogramming, there's docs4#Lean.Meta.withTransparency and specializations to particular transparencies.

[Heather Macbeth]

Thank you both! with_unfolding_all is what I was after.

I'm not sure I understand the difference between with_reducible and Lean.Parser.Tactic.withReducible. One is a syntax, the other is a ParserDescr? Would it be possible to have both versions indexed in the documentation?

[Heather Macbeth]

I see I can ctrl-click from a use of with_reducible to the declaration Lean.Elab.Tactic.evalWithReducible, but is there a way to go in the other direction?

[Alex J. Best]

If you right click there should be both an option to go to definition and go to declaration, one of those takes you to where the parser is defined and one of them to where the elaborator is defined

[Heather Macbeth]

Very instructive, thank you! I had never even realised there was a difference.

[Sebastian Ullrich]

The distinction is a bit arbitrary. Now that we have go to definition with a choice of targets with https://github.com/leanprover/lean4/pull/1767, I was wondering whether we should simply do the same here and drop go to declaration.