Lean4
/-- The command `#conv tac => e` will run a conv tactic `tac` on `e`, and display the resulting
expression (discarding the proof).
For example, `#conv rw [true_and_iff] => True ∧ False` displays `False`.
There are also shorthand commands for several common conv tactics:
* `#whnf e` is short for `#conv whnf => e`
* `#simp e` is short for `#conv simp => e`
* `#norm_num e` is short for `#conv norm_num => e`
* `#push_neg e` is short for `#conv push_neg => e`
-/
@[command_parser 1000]
public meta def «command#conv_=>_» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Conv.«command#conv_=>_» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "#conv ") (ParserDescr.cat✝ `conv 0))
(ParserDescr.symbol✝ " => "))
(ParserDescr.cat✝ `term 0))
