Lean 4 analogue with `decl_name`

Stream: lean4

[Scott Morrison]

In Lean 3 we had

/-- Name of the declaration currently being elaborated. -/
meta constant decl_name : tactic name

What is the Lean 4 analogue?

[Mario Carneiro]

decl_name%, a term macro which expands to a name literal (it's super convenient)

[Mario Carneiro]

there is also a plumbing version of the function if you need it

[David Renshaw]

https://github.com/leanprover/lean4/blob/d7d61bfb558ffcdff599249297c50d8b65c4aeb4/src/Lean/Elab/BuiltinTerm.lean#L216-L219
delegates to
https://github.com/leanprover/lean4/blob/d7d61bfb558ffcdff599249297c50d8b65c4aeb4/src/Lean/Elab/Term.lean#L399
which reads
https://github.com/leanprover/lean4/blob/d7d61bfb558ffcdff599249297c50d8b65c4aeb4/src/Lean/Elab/Term.lean#L157