theorem_proving_in_lean4 icon indicating copy to clipboard operation
theorem_proving_in_lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

Some graphics missing in VSCodium

Open navidrashidian opened this issue 11 months ago • 2 comments

Hi,

I am reading Theorem Proving in Lean 4 on VSCodium. I have installed the common lean4 extension. But some graphics is missing as evidences by this picture? image I would be grateful if you could help me fix the problem.

navidrashidian avatar Mar 16 '24 12:03 navidrashidian

Can you write down precisely what you did to open this in the editor? Normally I'd read it in Firefox or a browser. That'll help me look into what needs fixing, and see if I can reproduce it.

Thanks!

david-christiansen avatar Mar 21 '24 22:03 david-christiansen

I press Ctrl+Shift+P and then type ">lean 4:docview:opendocview." The rest is obvious. Another problem I face is that the left and right keys on my keyboard work very strangely when I open theorem proving in lean.

navidrashidian avatar Mar 22 '24 17:03 navidrashidian