clean% term elaborator

Remove identity functions from a term.

def Lean.Expr.cleanConsts : List Lean.Name

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

Equations

• Lean.Expr.cleanConsts = [`id]

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

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.

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

Equations

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

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

Equations

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

def Mathlib.Tactic.tacticClean_ : Lean.ParserDescr

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

Equations

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