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