toAdditiveAttrOption

Mathlib.Tactic.ToAdditive.Frontend

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

Lean4

/-- An `attr := ...` option for `to_additive`. -/
meta def toAdditiveAttrOption : Lean.ParserDescr✝ :=
  ParserDescr.nodeWithAntiquot✝ "toAdditiveAttrOption" `ToAdditive.toAdditiveAttrOption
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "attr" false✝)
        (ParserDescr.symbol✝ " := "))
      ((with_annotate_term"sepBy(" @ParserDescr.sepBy✝) (ParserDescr.parser✝ `Lean.Parser.Term.attrInstance) ","
        (ParserDescr.symbol✝ ", ") Bool.false✝))

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

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

Разделы

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

Аффилиация

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