This version is outdated. Go to lean-lang.org
11 Matching Annotations
- Aug 2025
-
leanprover.github.io leanprover.github.io
-
-
This is a free book on using Lean 4 as a programming language. All code samples are tested with Lean 4 release 4.1.0.
This version is outdated. Go to lean-lang.org
-
-
leanprover.github.io leanprover.github.io
-
Copyright Microsoft Corporation 2023 This is a free book on using Lean 4 as a programming language. All code samples are tested with Lean 4 release 4.1.0.
This version is outdated. Go to lean-lang.org
-
-
leanprover.github.io leanprover.github.io
-
When the filename points to a directory, it is shown with a helper, and then its contents are recursively shown in a new configuration in which the prefix has been extended to account for being in a new directory.
For behavior in new versions of Lean, go to up-to-date version of the book
-
-
leanprover.github.io leanprover.github.io
-
repeat makes use of a type whose ForM instance is partial.
repeatis a piece of syntax and cannot be checked for definition (at least I failed to do so).
-
-
leanprover.github.io leanprover.github.io
-
The second argument has a type that begins with Unit → to allow the definition of seq to short-circuit in cases where the function will never be applied.
Remember that this is needed because Lean is eager and strict, as opposed to Haskell
-
-
leanprover.github.io leanprover.github.io
-
large := size == Size.large
This works precisely because the structure is immutable
-
Structures and Inheritance
This is not in Haskell or Ocaml; it's nice to see how Lean approach subtyping problems, the desugaring resembles IRs from major compilers from other languages.
-
-
leanprover.github.io leanprover.github.io
-
andThen
You'd encounter this verbatim in Rust
-
-
leanprover.github.io leanprover.github.io
-
Multiple structures may have fields with the same names.
A lesson learnt from Haskell
-
-
leanprover.github.io leanprover.github.io
-
rather than to zero-argument functions
For a thunk, do
def lazyHello : Thunk String := fun () => "world" -- abbrev Thunk (α : Type) := Unit → α -- built-in
-