fp-lean
fp-lean copied to clipboard
leanprover
Functional Programming in Lean
File: [functional-programming-lean/src/monad-transformers.md](https://github.com/leanprover/fp-lean/blob/master/functional-programming-lean/src/monad-transformers.md) Sentence: "A concrete monad can be build from a collection of monad transformers, which enables much more code re-use." Word "build" should be "built" Awesome book btw!
A reference to a function `dbEq` is made in section _A Universe of Data_ in the following sentence: > The definition of dbEq can be used to define a BEq...
In sections 10.3 and onward, users are introduced to `termination_by`. I think the phrasing of this has changed recently in Lean, for example the definition of `arrayMapHelper` doesn't work for...
Please quote the text that is incorrect: > echo "It works!" | ./build/bin/feline In what way is this incorrect? The path in here should be ./.lake/build/bin/feline. Because the current path...
The following is given in the Typed Queries [exercise](https://lean-lang.org/functional_programming_in_lean/dependent-types/typed-queries.html#exercises) > [Nullable Types](https://lean-lang.org/functional_programming_in_lean/dependent-types/typed-queries.html#nullable-types) > Add support for nullable columns to the query language by representing database types with the following structure:...
In Lean v4.3.0, "`simp` will no longer try to use Decidable instances to rewrite terms" by default ([release notes](https://github.com/leanprover/lean4/releases/tag/v4.3.0)). This change broke these proofs in chapter 3: ``` lean theorem...
Please quote the text that is incorrect: ``` echo "It works!" | ./build/bin/feline ``` In what way is this incorrect? This works in `bash`, but in VS Code, the default...
See the suggested changes in PR 149: https://github.com/leanprover/fp-lean/pull/149/files
`theorem onePlusOneAndLessThan : 1 + 1 = 2 ∨ 3 < 5 := by simp`
Please quote the text that is incorrect: > To build the package, run the command `lake build`. After a number of build commands scroll by, the resulting binary has been...
