toAdditiveOption

Mathlib.Tactic.ToAdditive.Frontend

URI: https://scilib.ai/kg/mathlib#ToAdditive.toAdditiveOption

Lean4

/-- Options to `to_additive`. -/
meta def toAdditiveOption : Lean.ParserDescr✝ :=
  ParserDescr.nodeWithAntiquot✝ "toAdditiveOption" `ToAdditive.toAdditiveOption
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "(")
        (ParserDescr.binary✝ `orelse ToAdditive.toAdditiveAttrOption
          (ParserDescr.binary✝ `orelse ToAdditive.toAdditiveReorderOption
            (ParserDescr.binary✝ `orelse ToAdditive.toAdditiveRelevantOption
              ToAdditive.toAdditiveDontTranslateOption))))
      (ParserDescr.symbol✝ ")"))

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru