Open alok opened 2 months ago
I looked in lean-vscode for the relevant code to impl this but no luck. Since it's meant to be run interactively, why not elim a context switch?
I looked in lean-vscode for the relevant code to impl this but no luck. Since it's meant to be run interactively, why not elim a context switch?