`clean%`

term elaborator #

Remove identity functions from a term.

List of names removed by the `clean`

tactic.
All of these names must resolve to functions defeq `id`

.

## Equations

- Lean.Expr.cleanConsts = [`id]

## Instances For

Clean an expression by eliminating identify functions listed in `cleanConsts`

.
Also eliminates `fun x => x`

applications and tautological `let_fun`

bindings.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`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:

```
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
```

## Equations

- Mathlib.Tactic.cleanStx = Lean.ParserDescr.node `Mathlib.Tactic.cleanStx 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "clean% ") (Lean.ParserDescr.cat `term 0))

## Instances For

`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:

```
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
```

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

(Deprecated) `clean t`

is a macro for `exact clean% t`

.

## Equations

- One or more equations did not get rendered due to their size.