@@ -57,6 +57,16 @@ The Infoview *lean.infoview*
5757 Infoview-specific interaction for customizing or controlling the display of
5858 Lean's interactive goal state.
5959
60+ InfoviewViewOptions *InfoviewViewOptions*
61+
62+ Fields: ~
63+ {show_types} (boolean) show type hypotheses
64+ {show_instances} (boolean) show instance hypotheses
65+ {show_hidden_assumptions} (boolean) show hypothesis names which are inaccessible
66+ {show_let_values} (boolean) show let-value bodies
67+ {reverse} (boolean) order hypotheses bottom-to-top
68+
69+
6070Pin *Pin*
6171 An individual pin.
6272
@@ -92,6 +102,13 @@ InfoviewNewArgs *InfoviewNewArgs*
92102 {horizontal_position?} ()
93103
94104
105+ FilterSelection *FilterSelection*
106+
107+ Fields: ~
108+ {description} (string)
109+ {option} (string)
110+
111+
95112infoview.close_all() *infoview.close_all*
96113 Close all open infoviews (across all tabs).
97114
@@ -180,6 +197,13 @@ infoview.reposition() *infoview.reposition*
180197 Does nothing if there are more than 2 open windows.
181198
182199
200+ infoview.select_view_options() *infoview.select_view_options*
201+ Interactively set some view options for the infoview.
202+
203+ Does not persist the selected options; if you wish to permanently affect
204+ which hypotheses are shown, set them in your lean.nvim configuration.
205+
206+
183207==============================================================================
184208(Unicode) Abbreviation Expansion *lean.abbreviations*
185209
0 commit comments