| These examples are checked in Lean's CI to ensure that they continue | |
| to work. They are included in the documentation section of the Lean | |
| website via a script that copies the latest version, in order to | |
| ensure that the website tracks Lean releases rather than `master`. |