Lean4
/-- The command `#whnf e` evaluates `e` to Weak Head Normal Form, which means that the "head"
of the expression is reduced to a primitive - a lambda or forall, or an axiom or inductive type.
It is similar to `#reduce e`, but it does not reduce the expression completely,
only until the first constructor is exposed. For example:
```
open Nat List
set_option pp.notation false
#whnf [1, 2, 3].map succ
-- cons (succ 1) (map succ (cons 2 (cons 3 nil)))
#reduce [1, 2, 3].map succ
-- cons 2 (cons 3 (cons 4 nil))
```
The head of this expression is the `List.cons` constructor,
so we can see from this much that the list is not empty,
but the subterms `Nat.succ 1` and `List.map Nat.succ (List.cons 2 (List.cons 3 List.nil))` are
still unevaluated. `#reduce` is equivalent to using `#whnf` on every subexpression.
-/
@[command_parser 1000]
public meta def «command#whnf_» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Conv.«command#whnf_» 1022
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "#whnf ") (ParserDescr.cat✝ `term 0))
