plugins.lean.infoview.lean3.mouseEvents

Setting this to true will simulate mouse events in the Lean 3 infoview, this is buggy at the moment so you can use the I/i keybindings to manually trigger these.

Plugin default: false

Type: null or boolean or raw lua code

Default: null

Declared by:

plugins.lean.infoview.lean3.showFilter

Plugin default: true

Type: null or boolean or raw lua code

Default: null

Declared by: