Lean4
/-- The basic usage is `#norm_num e`, where `e` is an expression,
which will print the `norm_num` form of `e`.
Syntax: `#norm_num` (`only`)? (`[` simp lemma list `]`)? `:`? expression
This accepts the same options as the `#simp` command.
You can specify additional simp lemmas as usual, for example using `#norm_num [f, g] : e`.
(The colon is optional but helpful for the parser.)
The `only` restricts `norm_num` to using only the provided lemmas, and so
`#norm_num only : e` behaves similarly to `norm_num1`.
Unlike `norm_num`, this command does not fail when no simplifications are made.
`#norm_num` understands local variables, so you can use them to introduce parameters.
-/
@[command_parser 1000]
public meta def normNumCmd : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.normNumCmd 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "#norm_num") Lean.Parser.Tactic.optConfig)
(ParserDescr.unary✝ `optional ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) " only" false✝)))
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.simpArgs))
(ParserDescr.unary✝ `optional (ParserDescr.symbol✝ " :")))
(ParserDescr.unary✝ `group (ParserDescr.const✝ `ppSpace)))
(ParserDescr.cat✝ `term 0))
