Skip to content

Commit

Permalink
Further link gardening
Browse files Browse the repository at this point in the history
  • Loading branch information
david-christiansen committed Feb 6, 2024
1 parent 2b8338e commit 6c534da
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions functional-programming-lean/src/next-steps.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,11 @@ Depending on your interests, the following resources might be useful for learnin

Lean 4 itself is described in the following resources:

* [Theorem Proving in Lean 4](https://leanprover.github.io/theorem_proving_in_lean4/) is a tutorial on writing proofs using Lean.
* [The Lean 4 Manual](https://leanprover.github.io/lean4/doc/) provides a reference for the language and its features. At the time of writing, it is still incomplete, but it describes many aspects of Lean in greater detail than this book.
* [Theorem Proving in Lean 4](https://lean-lang.org/theorem_proving_in_lean4/) is a tutorial on writing proofs using Lean.
* [The Lean 4 Manual](https://lean-lang.org/lean4/doc/) provides a reference for the language and its features. At the time of writing, it is still incomplete, but it describes many aspects of Lean in greater detail than this book.
* [How To Prove It With Lean](https://djvelleman.github.io/HTPIwL/) is a Lean-based accompaniment to the well-regarded textbook [_How To Prove It_](https://www.cambridge.org/highereducation/books/how-to-prove-it/6D2965D625C6836CD4A785A2C843B3DA) that provides an introduction to writing paper-and-pencil mathematical proofs.
* [Metaprogramming in Lean 4](https://github.com/arthurpaulino/lean4-metaprogramming-book) provides an overview of Lean's extension mechanisms, from infix operators and notations to macros, custom tactics, and full-on custom embedded languages.
* [Functional Programming in Lean](https://leanprover.github.io/functional_programming_in_lean/) may be interesting to readers who enjoy jokes about recursion.
* [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/) may be interesting to readers who enjoy jokes about recursion.

However, the best way to continue learning Lean is to start reading and writing code, consulting the documentation when you get stuck.
Additionally, the [Lean Zulip](https://leanprover.zulipchat.com/) is an excellent place to meet other Lean users, ask for help, and help others.
Expand Down

0 comments on commit 6c534da

Please sign in to comment.