From 885deec745cf52c86676d9462bcbd98341cd1866 Mon Sep 17 00:00:00 2001 From: Chris Lovett Date: Mon, 6 Jun 2022 17:48:41 -0700 Subject: [PATCH] doc: add link to short quickstart video --- doc/quickstart.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/quickstart.md b/doc/quickstart.md index e66f27ac94..4c5dd396c1 100644 --- a/doc/quickstart.md +++ b/doc/quickstart.md @@ -3,6 +3,8 @@ These instructions will walk you through setting up Lean using the "basic" setup and VS Code as the editor. See [Setup](./setup.md) for other ways, supported platforms, and more details on setting up Lean. +See quick [walkthrough demo video](https://www.youtube.com/watch?v=yZo6k48L0VY). + 1. Install [VS Code](https://code.visualstudio.com/). 1. Launch VS Code and install the `lean4` extension.