leanprover / theorem_proving_in_lean4

Theorem Proving in Lean 4
https://leanprover.github.io/theorem_proving_in_lean4/
Apache License 2.0
146 stars 82 forks source link

Some graphics missing in VSCodium #109

Open navidrashidian opened 3 months ago

navidrashidian commented 3 months ago

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.

david-christiansen commented 3 months ago

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!

navidrashidian commented 3 months ago

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.