chore: add link from Lean 4 manual to FP in Lean

This commit is contained in:
Leonardo de Moura 2022-06-09 16:28:54 -07:00
parent 0ac863b353
commit 97e689d670
2 changed files with 8 additions and 0 deletions

View file

@ -5,6 +5,7 @@
- [Setting Up Lean](./quickstart.md)
- [Extended Setup Notes](./setup.md)
- [Theorem Proving in Lean](./tpil.md)
- [Functional Programming in Lean](fplean.md)
- [Examples](./examples.md)
- [Palindromes](examples/palindromes.lean.md)
- [Binary Search Trees](examples/bintree.lean.md)

7
doc/fplean.md Normal file
View file

@ -0,0 +1,7 @@
Functional Programming in Lean
=======================
The goal of [this book](https://leanprover.github.io/functional_programming_in_lean/) is to be an accessible introduction to using Lean 4 as a programming language.
It should be useful both to people who want to use Lean as a general-purpose programming language and to mathematicians who want to develop larger-scale proof automation but do not have a background in functional programming.
It does not assume any background with functional programming, though it's probably not a good first book on programming in general.
New content will be added once per month until it's done.