Code snippets that claim to present how things are defined in core Lean. Since Kyle's notation rehaul, those are broken as we need to name the notation to avoid a clash. I've decided nobody would try to run those snippets anyway.
u and v from the Diaconescu's theorem section. Lean complains they are computable, which is of course nonsense (unless it's because they are Props?), and certainly goes against the pedagogical point of the section.
The updated imports are not minimal, but instead sensible ones that we want people to know. I paid attention to having a single import per snippet.
The update is not to bleeding-edge mathlib, so there's still the risk that people will try running the snippets on their newer mathlib install. However, not much has changed since January, and I haven't personally spotted anything that would need further changes.
Update all code snippets to make sure they run without error nor warning on https://github.com/leanprover-community/mathlib/commit/feb165c980c918bb296fede8c3b21dbb4b85bb56, which is the commit the Lean web editor runs on. Exceptions are:
uandvfrom the Diaconescu's theorem section. Lean complains they are computable, which is of course nonsense (unless it's because they are Props?), and certainly goes against the pedagogical point of the section.The updated imports are not minimal, but instead sensible ones that we want people to know. I paid attention to having a single import per snippet.
The update is not to bleeding-edge mathlib, so there's still the risk that people will try running the snippets on their newer mathlib install. However, not much has changed since January, and I haven't personally spotted anything that would need further changes.
Closes #110 Closes #117 Closes #118