lean4-metaprogramming-book icon indicating copy to clipboard operation
lean4-metaprogramming-book copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Add to vscode docview?

Open alok opened this issue 1 year ago • 0 comments
trafficstars

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?

2024-05-01-17-39-21

alok avatar May 02 '24 00:05 alok