You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The option to collapse/expand trace nodes is extremely helpful when navigating e.g. typeclass synthesis traces. But at least with my setup (Doom Emacs + lean4-mode), the traces are always fully expanded with no option to collapse them. Could we get this capability as well?
The text was updated successfully, but these errors were encountered:
This would be great to have, but honestly I don't see anyone putting that much work into the Emacs mode, which would also feel like kind of a waste given the dearth of users. Probably the most realistic solution would be to get the entire HTML info view either inside or at least next to Emacs.
The option to collapse/expand trace nodes is extremely helpful when navigating e.g. typeclass synthesis traces. But at least with my setup (Doom Emacs + lean4-mode), the traces are always fully expanded with no option to collapse them. Could we get this capability as well?
The text was updated successfully, but these errors were encountered: