File tree Expand file tree Collapse file tree 1 file changed +0
-14
lines changed Expand file tree Collapse file tree 1 file changed +0
-14
lines changed Original file line number Diff line number Diff line change @@ -9,7 +9,6 @@ Loogle ····································
9
9
satellite.nvim integration ···································· | lean.satellite |
10
10
LSP ································································· | lean.lsp |
11
11
Standard error buffers ··········································· | lean.stderr |
12
- Client-side sorrying ·············································· | lean.sorry |
13
12
14
13
==============================================================================
15
14
Introduction *lean.init*
@@ -392,17 +391,4 @@ stderr.enable() *stderr.enable*
392
391
Enable teeing stderr output somewhere (to a second visible buffer by default).
393
392
394
393
395
- ==============================================================================
396
- Client-side sorrying *lean.sorry*
397
-
398
- Support for sorrying multiple goals.
399
-
400
- You should generally prefer to use code actions for this functionality, but this module
401
- is maintained for a subset of users who prefer its behavior over the current code action
402
- behavior.
403
-
404
- sorry.fill() *sorry.fill*
405
- Fill the current cursor position with `sorry` s to discharge all goals.
406
-
407
-
408
394
vim:tw=78:ts=8:noet:ft=help:norl:
You can’t perform that action at this time.
0 commit comments