clean% term elaborator

Remove identity functions from a term.

def Lean.Expr.cleanConsts : List Name

List of names removed by the clean tactic. All of these names must resolve to functions defeq id.

def Lean.Expr.clean (e : Expr) : Expr

Clean an expression by eliminating identify functions listed in cleanConsts. Also eliminates fun x => x applications and tautological let/have bindings.

def Mathlib.Tactic.cleanStx : Lean.ParserDescr

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

def Mathlib.Tactic.elabClean : Lean.Elab.Term.TermElab

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

def Mathlib.Tactic.tacticClean_ : Lean.ParserDescr

(Deprecated) clean t is a macro for exact clean% t.