Enables the 'unnecessary <;>
' linter. This will warn whenever the <;>
tactic combinator
is used when ;
would work.
example : True := by apply id <;> trivial
The <;>
is unnecessary here because apply id
only makes one subgoal.
Prefer apply id; trivial
instead.
In some cases, the <;>
is syntactically necessary because a single tactic is expected:
example : True := by
cases () with apply id <;> apply id
| unit => trivial
In this case, you should use parentheses, as in (apply id; apply id)
:
example : True := by
cases () with (apply id; apply id)
| unit => trivial
Gets the value of the linter.unnecessarySeqFocus
option.
The multigoal
attribute keeps track of tactics that operate on multiple goals,
meaning that tac
acts differently from focus tac
. This is used by the
'unnecessary <;>
' linter to prevent false positives where tac <;> tac'
cannot
be replaced by (tac; tac')
because the latter would expose tac
to a different set of goals.
The
<;>
node itself.stx : Lean.Syntaxtrue
: this<;>
has been used unnecessarily at least oncefalse
: it has never been executed- If it has been used properly at least once, the entry is removed from the table.
used : Bool
The information we record for each <;>
node appearing in the syntax.
Instances For
The monad for collecting used tactic syntaxes.
True if this is a <;>
node in either tactic
or conv
classes.
Equations
- Std.Linter.UnnecessarySeqFocus.isSeqFocus k = (k == `Lean.Parser.Tactic.tactic_<>_ || k == `Lean.Parser.Tactic.Conv.conv_<>_)
Accumulates the set of tactic syntaxes that should be evaluated at least once.
Traverse the info tree down a given path.
Each (n, i)
means that the array must have length n
and we will descend into the i
'th child.
Equations
- One or more equations did not get rendered due to their size.
- Std.Linter.UnnecessarySeqFocus.getPath x x [] = some x
Search for tactic executions in the info tree and remove executed tactic syntaxes.
Search for tactic executions in the info tree and remove executed tactic syntaxes.
The main entry point to the unused tactic linter.
Equations
- One or more equations did not get rendered due to their size.