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 information we record for each <;>
node appearing in the syntax.
- stx : Lean.Syntax
The
<;>
node itself. - used : Bool
true
: 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.
The monad for collecting used tactic syntaxes.
True if this is a <;>
node in either tactic
or conv
classes.
Equations
- Batteries.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.
- Batteries.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.
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
Equations
- One or more equations did not get rendered due to their size.