`clean%`

term elaborator #

Remove identity functions from a term.

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

.
Also eliminates `fun x => x`

applications and tautological `let_fun`

bindings.

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

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

## Instances For

(Deprecated) `clean t`

is a macro for `exact clean% t`

.