From a5bf0d5ea5262e4442f5e71ea7a95df04852a1c6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Apr 2022 18:09:54 -0700 Subject: [PATCH] chore: invert setup chapters by making the quickstart the default and the other one "extended setup notes" --- doc/SUMMARY.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md index 1aa45b0022..5e0e5d80c4 100644 --- a/doc/SUMMARY.md +++ b/doc/SUMMARY.md @@ -2,8 +2,8 @@ - [What is Lean](./whatIsLean.md) - [Tour of Lean](./tour.md) -- [Setting Up Lean](./setup.md) - - [Quickstart](./quickstart.md) +- [Setting Up Lean](./quickstart.md) + - [Extended Setup Notes](./setup.md) - [Theorem Proving in Lean](./tpil.md) - [Examples](./examples.md) - [Palindromes](examples/palindromes.lean.md)