Lean4
/-- - `extract_goal` formats the current goal as a stand-alone theorem or definition after
cleaning up the local context of irrelevant variables.
A variable is *relevant* if (1) it occurs in the target type, (2) there is a relevant variable
that depends on it, or (3) the type of the variable is a proposition that depends on a
relevant variable.
If the target is `False`, then for convenience `extract_goal` includes all variables.
- `extract_goal *` formats the current goal without cleaning up the local context.
- `extract_goal a b c ...` formats the current goal after removing everything that the given
variables `a`, `b`, `c`, ... do not depend on.
- `extract_goal ... using name` uses the name `name` for the theorem or definition rather than
the autogenerated name.
The tactic tries to produce an output that can be copy-pasted and just work,
but its success depends on whether the expressions are amenable
to being unambiguously pretty printed.
The tactic responds to pretty printing options.
For example, `set_option pp.all true in extract_goal` gives the `pp.all` form.
-/
@[tactic_parser 1000]
public meta def extractGoal : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.ExtractGoal.extractGoal 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "extract_goal" false✝)
Mathlib.Tactic.ExtractGoal.config)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " using ") (ParserDescr.const✝ `ident))))
