Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Suggestions for clarity #114

Open
wants to merge 11 commits into
base: master
Choose a base branch
from

Conversation

turibe
Copy link
Contributor

@turibe turibe commented May 6, 2024

Suggestions to clarify some possibly confusing items. Main ones 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 apply tactic example, showing what gets unified and how the subgoals are generated.

@@ -355,11 +355,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
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since there's only one expression in this example, using "last" makes one think that something other than the full expression is being referred to.

that adds two natural numbers:

```lean
def add (x y : Nat) :=
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

When the add (x y : Nat) example comes first, a newcomer might think that it's a function of two arguments (no currying). So it seems better to have add (x Nat) (y : Nat) come first, and then say that it can be abbreviated.

@@ -13,12 +13,14 @@ One strategy for proving assertions about objects defined in the
language of dependent type theory is to layer an assertion language
and a proof language on top of the definition language. But there is
no reason to multiply languages in this way: dependent type theory is
flexible and expressive, and there is no reason we cannot represent
flexible and expressive, and it turns out that we can represent
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Rewording this positively makes it more clear that the following discussion is not meant to be an example of layering languages on top. (This could, perhaps, be made a little more explicit still.)

@turibe turibe mentioned this pull request May 6, 2024
@avigad
Copy link
Collaborator

avigad commented May 27, 2024

@turibe @jdchristensen I apologize that it has taken me so long to find time to catch up on the PR and the discussion in #112. David is right that I am protective of things I have written, and I appreciate the sensitivity that both of you have shown. I have read over @turibe's proposed changes and they are generally very good. It's often hard to judge changes in isolation, but I plan to come back to TPIL soon to make revisions, so I think it makes sense to merge this PR as is, given that I'll have a chance to tinker with the text later.

@jdchristensen
Copy link
Contributor

@avigad Did you maybe mean to tag @david-christiansen instead of me?

@avigad
Copy link
Collaborator

avigad commented May 27, 2024

Indeed, I did -- sorry for the mistake!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants