Lean4
/-- `change? term` unifies `term` with the current goal, then suggests explicit `change` syntax
that uses the resulting unified term.
If `term` is not present, `change?` suggests the current goal itself. This is useful after tactics
which transform the goal while maintaining definitional equality, such as `dsimp`; those preceding
tactic calls can then be deleted.
```lean
example : (fun x : Nat => x) 0 = 1 := by
change? 0 = _ -- `Try this: change 0 = 1`
```
-/
@[tactic_parser 1000]
public meta def change? : Lean.ParserDescr✝ :=
ParserDescr.node✝ `change? 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "change?" false✝)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
(ParserDescr.cat✝ `term 0))))
