tacticWhnf__ — Mathlib

Lean4
/-- `whnf at loc` puts the given location into weak-head normal form.
This also exists as a `conv`-mode tactic.

Weak-head normal form is when the outer-most expression has been fully reduced, the expression
may contain subexpressions which have not been reduced.
-/
@[tactic_parser 1000]
public meta def tacticWhnf__ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.tacticWhnf__ 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "whnf" false✝)
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) Lean.Parser.Tactic.location)))
Похожие утверждения