Skip to content
| Marketplace
Sign in
Visual Studio Code>Other>Loogle LeanNew to Visual Studio Code? Get it now.
Loogle Lean

Loogle Lean

Shreyas Srinivas

|
535 installs
| (0) | Free
This extension implements support for using loogle inside vscode in any lean file
Installation
Launch VS Code Quick Open (Ctrl+P), paste the following command, and press enter.
Copied to clipboard
More Info

Loogle Lean

This extension is a vscode front end for accessing loogle

Usage

This extension has exactly one command Loogle Search. This command can be accessed in one of three ways:

  1. The keyboard shortcut : Ctrl+Shift+L (Mac: Cmd+Shift+L)
  2. The search icon on the editor tab next to the lean icon
  3. Open the vscode command palette with Ctrl+Shift+P and search for loogle.
  • Contact us
  • Jobs
  • Privacy
  • Manage cookies
  • Terms of use
  • Trademarks
© 2025 Microsoft