Remove lean4-keybinding-*
user options and dissolve other parts of lean4-settings.el
#88
Milestone
lean4-keybinding-*
user options and dissolve other parts of lean4-settings.el
#88
Lean4-Mode currently offers these variables:
From an user perspective, these user-options feel out of place because they expect to change the default key bindings of a package by customizing the respective keymap directly. And from perspective of a Elisp developer working on Lean4-Mode, I'd also prefer to deal with a single keymap rather than above-mentioned user-options together with a function like
lean4-set-keys
that enables them. Thus, I propose to remove these user-options.Secondly, I propose to completely dissolve the
lean4-settings.el
file, in the sense that each user-options that is defined there, should be moved to the Elisp file where it is used.The text was updated successfully, but these errors were encountered: