Lean4
/-- Replace the selected expression with a definitional unfolding.
- After each unfolding, we apply `whnfCore` to simplify the expression.
- Explicit natural number expressions are evaluated.
- Unfolds of class projections of instances marked with `@[default_instance]` are not shown.
This is relevant for notational type classes like `+`: we don't want to suggest `Add.add a b`
as an unfolding of `a + b`. Similarly for `OfNat n : Nat` which unfolds into `n : Nat`.
To use `unfold?`, shift-click an expression in the tactic state.
This gives a list of rewrite suggestions for the selected expression.
Click on a suggestion to replace `unfold?` by a tactic that performs this rewrite.
-/
@[tactic_parser 1000]
public meta def tacticUnfold? : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.InteractiveUnfold.tacticUnfold? 1024
(ParserDescr.nonReservedSymbol✝ "unfold?" false✝)
