max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix comment

Browse source
This commit is contained in:
Sebastian Ullrich 2021-05-05 15:08:30 +02:00
parent 456264bf31
commit 84d3896ea7
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Server/InfoUtils.lean
View file

@ -159,7 +159,7 @@ structure GoalsAtResult where
- None of the `children` can provide satisfy the condition above. That is, for composite tactics such as
`induction`, we always give preference for information stored in nested (children) tactics.
Moreover, we instruct the LSP server to use the state after the tactic execution if hoverPos >= endPos *and*
Moreover, we instruct the LSP server to use the state after the tactic execution if `hoverPos > pos` *and*
there is no nested tactic info (i.e. it is a leaf tactic; tactic combinators should decide for themselves
where to show intermediate/final states)
-/