Small fixes #112
Small fixes #112
Conversation
| you to express complex mathematical assertions, write complex hardware | ||
| and software specifications, and reason about both of these in a | ||
| and software specifications, and reason about all of these in a |
There was a problem hiding this comment.
"both" seems correct to me here - it's referring back to two things (assertions and specifications).
There was a problem hiding this comment.
Just to spell out the rationale for the suggestion, since the preceding text is "(a and (b and c))", the "both" causes the reader to do a bit more mental work to check the correspondence.
| numbers. (For those who like precise definitions, a Lean natural number | ||
| is an arbitrary-precision unsigned integer.) |
There was a problem hiding this comment.
This doesn't strike me as a correction, but more of a style change.
| The ``#check`` command asks Lean to report the type of a given expression | ||
| types; the `#eval` command asks Lean to evaluate the given expression. | ||
| Try declaring some constants and type checking some expressions on your | ||
| own; this is a good way to experiment with the system. |
There was a problem hiding this comment.
Successive sentences with semicolons is a bold choice - what about an em dash instead of the second one?
| @@ -145,8 +143,7 @@ its two components. | |||
| One way in which Lean's dependent type theory extends simple type | |||
| theory is that types themselves --- entities like ``Nat`` and ``Bool`` | |||
| --- are first-class citizens, which is to say that they themselves are | |||
| objects. For that to be the case, each of them also has to have a | |||
| type. | |||
| objects. For that to be the case, each must also have a type. | |||
There was a problem hiding this comment.
This strikes me as more of an authorial choice than a mistake to be corrected
| similarly polymorphic: | ||
|
|
||
| ```lean | ||
| #check Prod -- Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v) | ||
| ``` | ||
|
|
||
| To define polymorphic constants, Lean allows you to | ||
| To define polymorphic constants, Lean lets you |
There was a problem hiding this comment.
The original text seems fine to me
| Lean uses the keyword `fun` (or `λ`, entered as ``\lambda``) to create a function | ||
| from an expression, as follows: |
There was a problem hiding this comment.
The original text seems fine to me
There was a problem hiding this comment.
When previous unicode symbols have been introduced, the text shorthand was mentioned. This is the first time that lambda is mentioned, so it seems to be in order. It also connects the symbol with the use of "lambda" below, for any reader who might be unfamiliar with the greek symbol (admittedly, unlikely in this case).
| @@ -338,12 +335,12 @@ Think about what these expressions mean. The expression | |||
| ``fun x : Nat => x`` denotes the identity function on ``Nat``, the | |||
| expression ``fun x : Nat => true`` denotes the constant function that | |||
| always returns ``true``, and ``fun x : Nat => g (f x)`` denotes the | |||
| composition of ``f`` and ``g``. You can, in general, leave off the | |||
| composition of ``f`` and ``g``. You can, in general, skip the | |||
There was a problem hiding this comment.
The original text seems fine to me
| @@ -355,11 +352,11 @@ You can also pass types as parameters: | |||
| ```lean | |||
| #check fun (α β γ : Type) (g : β → γ) (f : α → β) (x : α) => g (f x) | |||
| ``` | |||
| The last expression, for example, denotes the function that takes | |||
| This last expression, for example, denotes the function that takes | |||
There was a problem hiding this comment.
The original text seems fine to me
There was a problem hiding this comment.
"This" instead of "the" makes it clearer that we are talking about the entire expression, not some subterm of it (perhaps even the subterm that comes last in the longer expression!). Perhaps a better fix would be, "The above expression, for example, ... "
| function that takes an input parameter `x` of type `Nat` and returns `x + x`, so its return type is `Nat`. | ||
| You can then invoke this function using: |
There was a problem hiding this comment.
The original text seems fine to me
|
|
||
| ```lean | ||
| # def double (x : Nat) : Nat := | ||
| # x + x | ||
| #eval double 3 -- 6 | ||
| ``` | ||
|
|
||
| In this case you can think of `def` as a kind of named `lambda`. | ||
| You can think of `def` as a kind of named `lambda`. |
There was a problem hiding this comment.
The original text seems fine to me
There was a problem hiding this comment.
Saying "In this case" leaves the lingering possibility in the reader's mind that def works differently in other cases... which it does, but it's not clear how general or specific "this case" is. Perhaps better: "When used to define functions, ..."
|
Thank you for putting in the time to improve the Lean docs! I made it a fair bit into this large PR, and I think that it's a bit much. Generally, the suggested changes seem to come in two categories:
I'm only really comfortable merging the first category of changes - this is a work by @avigad et al, not me, and I don't want to interfere with the voice and writing style of the authors. The majority are in the second category, but dropping repetitive comments to that effect into the PR seems like a bad way to use both your time and my time. Would it be possible to split the PR into two, separating the two kinds of changes? Then I can review and merge corrections, and leave the style suggestions to @avigad when he has time to look at the book again. Otherwise, sometime next week (almost out of work hours for this week), I can sit down with Thank you! |
|
OK, I will split the PR, and will make a new one with the more substantial suggestions. Thx. |
| assertions and proofs in the same general framework. | ||
|
|
||
| For example, we could introduce a new type, ``Prop``, to represent | ||
| As an example of layering languages on top, |
There was a problem hiding this comment.
Now I see that this is an example of using the same general framework; the "could/would" formulation below makes it a bit confusing. Saying, more directly, "... it turns out that we can represent assertions and proofs in the same general framework. For example..." , would help.
Streamline some language and add clarifications. The more substantial changes are:
Introducing arguments in a way consistent with the idea that functions really only take one argument at a time (currying); the current formulation might mislead the reader into thinking otherwise.
Expand the first
applytactic example, showing what gets unified and how the subgoals are generated.