Showing branching side-by-side

Stream: general

[Wrenna Robson]

I don't know if editor support could help here. Intuitively I want to put two branches side by side in two columns, but obviously that is hard to actually typeset. However in theory I wonder if VS Code, at least, could be prevailed upon to make this easier.

[Eric Wieser]

I don't see that (vscode support for parallel columns) being remotely likely

[Wrenna Robson]

Fair enough.

[Kenny Lau]

don't we have the colGt stuff

[Wrenna Robson]

Hmm?

[Notification Bot]

5 messages were moved here from #lean4 > Alternative and do-notation by Eric Wieser.

[Eric Wieser]

(moving the thread, since this could also apply to if, Sum.elim, etc)

[Wrenna Robson]

Yes, good point.

[Kenny Lau]

it might be very tricky if a command is two half-columns long tho, you can't really cut off in the middle of a syntax

[Wrenna Robson]

Yes. I mean I guess there's a reason why no (?) languages do it. I think what I was imagining was a difference between the file as stored in raw text and in the IDE.