Dependent Type Theory

Function Abstraction and Evaluation

There is a statement "...has nothing to do with the constant b declared earlier." but there is no such declaration of b. There is a b1 and a b2 back in Simple Type Theory.

Variables and Sections

When it is described how Lean automatically inserts variables that are used implicitly, is it worth mentioning anything about the order they are inserted?

Namespaces

It is noted that namespaces can be reopened. Perhaps worth mentioning that any definitions made after the namespace is reopened are added to the collection of definitions associated with the namespace.

Tactics

Basic Tactics

The tactics renameI and admit are not colour coded like other tactic names.

There is a statement "Here the rewrite tactic, abbreviated rw...". If rw is replaced by rewrite it is necessary to apply rfl to complete the proof, so rw is a little more than a simple abbreviation of rewrite.

Interacting with Lean

Importing Files

I don't quite get the sentence "One can also specify imports relative to the current directory; for example, Importing is transitive." How is transitivity of imports an example of import relative to the current directory?

Inductive Types

It is stated "The first character | in an inductive declaration is optional. We can also separate constructors using a comma instead of |." I am unable to either omit | or use a comma. However, it does parse if where is omitted (though where is not optional for structure declarations).

Using nightly 2021-09-12.

Induction and Recursion

Structural Recursion and Induction

It is stated "Thus both of the following proofs of zero_add work:". However, after the statement there is only one proof of zero_add.

leanprover / theorem_proving_in_lean4

A few comments #7