From 97e689d670a4759b27fb0ddc9007c1e5436507d8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Jun 2022 16:28:54 -0700 Subject: [PATCH] chore: add link from Lean 4 manual to FP in Lean --- doc/SUMMARY.md | 1 + doc/fplean.md | 7 +++++++ 2 files changed, 8 insertions(+) create mode 100644 doc/fplean.md diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md index 5938758ebe..72daebfdbd 100644 --- a/doc/SUMMARY.md +++ b/doc/SUMMARY.md @@ -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) diff --git a/doc/fplean.md b/doc/fplean.md new file mode 100644 index 0000000000..4f00130c6f --- /dev/null +++ b/doc/fplean.md @@ -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.