Lean4
/-- Normalize numerical expressions. Supports the operations `+` `-` `*` `/` `⁻¹` `^` and `%`
over numerical types such as `ℕ`, `ℤ`, `ℚ`, `ℝ`, `ℂ` and some general algebraic types,
and can prove goals of the form `A = B`, `A ≠ B`, `A < B` and `A ≤ B`, where `A` and `B` are
numerical expressions. It also has a relatively simple primality prover.
-/
@[tactic_parser 1000]
public meta def normNum : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.normNum 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "norm_num" false✝) Lean.Parser.Tactic.optConfig)
(ParserDescr.unary✝ `optional ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) " only" false✝)))
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.simpArgs))
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.location))
