toAdditiveDontTranslateOption — Mathlib

Lean4
/-- `dont_translate := ...` takes a list of type variables (separated by spaces) that should not be
considered for translation. For example in
```
lemma foo {α β : Type} [Group α] [Group β] (a : α) (b : β) : a * a⁻¹ = 1 ↔ b * b⁻¹ = 1
```
we can choose to only additivize `α` by writing `to_additive (dont_translate := β)`.
-/
meta def toAdditiveDontTranslateOption : Lean.ParserDescr✝ :=
  ParserDescr.nodeWithAntiquot✝ "toAdditiveDontTranslateOption" `ToAdditive.toAdditiveDontTranslateOption
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "dont_translate" false✝)
        (ParserDescr.symbol✝ " := "))
      (ParserDescr.unary✝ `many1 (ParserDescr.const✝ `ident)))
Похожие утверждения