lean4-mode icon indicating copy to clipboard operation
lean4-mode copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Support collapsible trace nodes

Open JLimperg opened this issue 1 year ago • 3 comments

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?

JLimperg avatar Mar 28 '23 16:03 JLimperg