Def ToAdditive.will.getDontTranslates

Modification history

2025-08-27 23:00

Mathlib/Tactic/ToAdditive/Frontend.lean

feat(to_additive): `(dont_translate := ...)` option (#28637) …

Added ToAdditive.will.getDontTranslates View on Github →