From 7ed5625c4de99840d6b9171b6bf87b79e865f065 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 4 Feb 2025 14:58:33 +0100 Subject: [PATCH] update link to reference manual (#585) --- templates/learn.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/templates/learn.md b/templates/learn.md index e0989b259..3fa2faf26 100644 --- a/templates/learn.md +++ b/templates/learn.md @@ -55,7 +55,7 @@ doing Lean exercises on the fly: It also has useful information about the type theory of Lean, and an associated VSCode project with exercises. If you want something more focused on Lean itself than on using Lean, then you -can read the [reference manual](https://lean-lang.org/lean4/doc/). +can read the [reference manual](https://lean-lang.org/doc/reference/latest/) ([old manual](https://lean-lang.org/lean4/doc/)). ## (Meta)-programming and tactic writing