to_additive_dont_translate — Mathlib

Lean4

/-- The `to_additive_dont_translate` attribute, used to specify types that should be translated by
`to_additive`, but its operations should remain multiplicative.

Usage notes:
* Apply this together with the `to_additive` attribute.
* The name generation of `to_additive` is not aware that the operations on this type should not be
  translated, so you generally have to specify the name itself, if the name should remain
  multiplicative.
-/
@[attr_parser 1000]
public meta def to_additive_dont_translate : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `ToAdditive.to_additive_dont_translate 1024
    (ParserDescr.nonReservedSymbol✝ "to_additive_dont_translate" false✝)

Похожие утверждения