Lean4
/-- `clean% t` fully elaborates `t` and then eliminates all identity functions from it.
Identity functions are normally generated with terms like `show t from p`,
which translate to some variant on `@id t p` in order to retain the type.
These are also generated by tactics such as `dsimp` to insert type hints.
Example:
```lean
def x : Id Nat := by dsimp [Id]; exact 1
#print x
-- def x : Id Nat := id 1
def x' : Id Nat := clean% by dsimp [Id]; exact 1
#print x'
-- def x' : Id Nat := 1
```
-/
@[term_parser 1000]
public meta def cleanStx : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.cleanStx 1022
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "clean% ") (ParserDescr.cat✝ `term 0))
