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
.