tacticAlgebraize_only__ — Mathlib

Lean4

/-- Version of `algebraize`, which only adds `Algebra` instances and `IsScalarTower` instances,
but does not try to add any instances about any properties tagged with
`@[algebraize]`, like for example `Finite` or `IsIntegral`. -/
@[tactic_parser 1000]
public meta def tacticAlgebraize_only__ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.tacticAlgebraize_only__ 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "algebraize_only" false✝)
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) Mathlib.Tactic.algebraizeTermSeq)))

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