Lean 4 shows inaccessible hypotheses with a trailing cross symbol.
Emacs and VSCode treat these by doing one or both of eliding the cross symbol and highlighting the hypotheses in a dimmer color. We should likely follow suit in some way.
(Follow the resolution in the Zulip thread most likely)
Lean 4 shows inaccessible hypotheses with a trailing cross symbol.
Emacs and VSCode treat these by doing one or both of eliding the cross symbol and highlighting the hypotheses in a dimmer color. We should likely follow suit in some way.
(Follow the resolution in the Zulip thread most likely)