fp-lean/book/FPLean.lean at master · leanprover/fp-lean · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
import VersoManual

import FPLean.Intro
import FPLean.Acks
import FPLean.GettingToKnow
import FPLean.HelloWorld
import FPLean.PropsProofsIndexing
import FPLean.TypeClasses
import FPLean.Monads
import FPLean.FunctorApplicativeMonad
import FPLean.MonadTransformers
import FPLean.DependentTypes
import FPLean.TacticsInductionProofs
import FPLean.ProgramsProofs
import FPLean.NextSteps

open Verso.Genre Manual
open Verso Code External

open Verso Doc Elab in
open Lean (quote) in
@[role_expander versionString]
def versionString : RoleExpander
  | #[], #[] => do
    let version ← IO.FS.readFile "../examples/lean-toolchain"
    let version := version.trimAscii.dropPrefix "leanprover/lean4:" |>.copy
    pure #[← ``(Verso.Doc.Inline.code $(quote version))]
  | _, _ => throwError "Unexpected arguments"


#doc (Manual) "Functional Programming in Lean" =>

%%%
authors := ["David Thrane Christiansen"]
%%%


_Copyright Microsoft Corporation 2023 and Lean FRO, LLC 2023–2026_


This is a free book on using Lean as a programming language. All code samples are tested with Lean release {versionString}[].

{include 1 FPLean.Intro}

{include 1 FPLean.Acks}

{include 1 FPLean.GettingToKnow}

{include 1 FPLean.HelloWorld}

{include 1 FPLean.PropsProofsIndexing}

{include 1 FPLean.TypeClasses}

{include 1 FPLean.Monads}

{include 1 FPLean.FunctorApplicativeMonad}

{include 1 FPLean.MonadTransformers}

{include 1 FPLean.DependentTypes}

{include 1 FPLean.TacticsInductionProofs}

{include 1 FPLean.ProgramsProofs}

{include 1 FPLean.NextSteps}