Trim Tactic Compatibility

This file provides a lightweight compatibility tactic for normalizing associative expressions.

Main declarations

• trim

def tacticTrim : Lean.ParserDescr

trim is a lightweight replacement for the Lean 3 tactic that normalized chains of associative operations such as list concatenation. In Lean 4 the same effect can usually be achieved by simp with the standard associativity/identity lemmas, so we expose it as a convenient macro to keep the existing proofs readable.

Equations

• tacticTrim = Lean.ParserDescr.node `tacticTrim 1024 (Lean.ParserDescr.nonReservedSymbol "trim" false)