fp-lean
fp-lean copied to clipboard
leanprover
Functional Programming in Lean
## Option At this point in the text, reading linearly, universes have not yet been introduced and I could not figure out what this syntax meant (the `: Type`) and...
Thanks a lot for the book. I've really enjoyed working through it so far and the quality is great. I had a couple of things that slightly confused me, maybe...
This section suggests `main` can only have 3 different types: https://github.com/leanprover/fp-lean/blob/60624372e1b7f85967de2f9f2c906fb351e0469a/functional-programming-lean/src/hello-world/summary.md?plain=1#L16-L20 I think `main : List String → IO Unit` is a 4th alternative, which lean seems to accept just...
`IO.println` is a function from strings to `IO` actions that, when executed, *writes* the given string to standard output.
`occaisionally` => occasionally `head!` is used with no earlier explanation of what the `!` means. I think it would be helpful to add a reminder after this paragraph that in...
It's been confusing [for at least one reader](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/First.20maintenance.20release.20of.20Functional.20Programming.20in.20Lean) - the text probably assumes more knowledge of Unix lore than it should.
Auto-implicits can lead to confusing error messages, so the book should discuss them. An example that occurred recently on Zulip: ``` structure RectangularPrism where height: Float width: Float depth: float...
> For the base instance, it is necessary to write `OfNat Even Nat.zero` instead of `OfNat Even 0`. After was closed, `OfNat` instances defined with `Nat` literals could be resolved...
Maybe typo. The functions defined in the previous section shall be right, but here, the functions will give unwanted result. Before. ``` bin/ │ hello.hash │ hello.trace │ hello ```...
On Mastodon, it was pointed out that Pandoc is good at consuming the print HTML file and producing an epub. If this will work for making a good epub, then...