Zulip Chat Archive
Stream: new members
Topic: Multiple Lean InfoViews in VScode?
Ching-Tsun Chou (Jul 10 2025 at 17:29):
Solved in #lean4 > Multiple Lean InfoViews in VScode?
Is it possible to have multiple Lean InforViews for multiple Lean files in VScode?
Last updated: Dec 20 2025 at 21:32 UTC