Typo in Tutorial

[kevinsullivan]

Prerequisites

• [ X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Tutorial (3.3) says, "Indeed, in dependent type theory (and in Lean), the Pi construction is fundamental, and α → β is just notation for Π x : α, β when β does not depend on α."

I believe it should say, "Indeed, in dependent type theory (and in Lean), the Pi construction is fundamental, and α → β is just notation for Π x : α, β when β does not depend on x."

Steps to Reproduce

See tutorial.

Expected behavior: [What you expect to happen]

See above.

Actual behavior: [What actually happens]

See above.

Reproduces how often: [What percentage of the time does it reproduce?]

100%

Versions

You can get this information from copy and pasting the output of lean --version, please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

[digama0]

I think this issue is for https://github.com/leanprover/theorem_proving_in_lean/issues .

[kevinsullivan]

Oops, thanks. Moving. --Kevin