max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/doc/quickstart.md
Marc Huisinga f74516a032
doc: update quickstart guide to reference vs code setup guide (#2968) 
Since the vscode-lean4 setup guide allows us to provide information on
setting up Lean 4 tailored to the user's operating system, this PR
adjusts the quickstart guide to reference the vscode-lean4 setup guide
instead.
2023-12-12 08:36:27 +00:00

993 B
Raw Blame History

Quickstart

These instructions will walk you through setting up Lean 4 together with VS Code as an editor for Lean 4. See Setup for supported platforms and other ways to set up Lean 4.

  1. Install VS Code.

  2. Launch VS Code and install the lean4 extension by clicking on the "Extensions" sidebar entry and searching for "lean4".

    installing the vscode-lean4 extension

  3. Open the Lean 4 setup guide by creating a new text file using "File > New Text File" (Ctrl+N), clicking on the ∀-symbol in the top right and selecting "Documentation… > Setup: Show Setup Guide".

    show setup guide

  4. Follow the Lean 4 setup guide. It will walk you through learning resources for Lean 4, teach you how to set up Lean's dependencies on your platform, install Lean 4 for you at the click of a button and help you set up your first project.

    setup guide