Floris van Doorn

> Leo is on vacation now. I'll check what I can do with this. This is not at all high priority, so don't worry too much if this is something...

Similar idea by Bryan: make a separate page showing all localized information.

I think the issue here is that you're documenting exceptions as the rule. The goal is to have propositions `UpperCamelCased`, with very few exceptions. E.g. https://github.com/leanprover/lean4/pull/1897 shows that we want...

Yes, I'm happy if you state the existence of exceptions. My preference is that we remove the `class LT` example, since that itself is an exception. If we keep it,...

Yes, it's a mess, and we should unify the instructions. I believe that https://leanprover-community.github.io/install/project.html is the easiest to find, so we need to make sure we keep that updated. We...

Should I also add [How to Prove it With Lean](https://djvelleman.github.io/HTPIwL/How-To-Prove-It-With-Lean.pdf)? [Logic and Mechanized Reasoning](https://avigad.github.io/lamr/logic_and_mechanized_reasoning.pdf) falls outside the scope of this page, I think.

I kept the meetings that were aimed at beginners, and removed the ones that weren't. We can remove more if you think that is appropriate.

This also had this happen to a student just now. * Is this caused by the root file not existing/not importing anything? (that was something we fixed afterwards). * What...

Additional suggestions: * Would it be possible to have a command `lake update-toolchain` which asks Github for the latest (release candidate) version of Lean, and replaces the `lean-toolchain` file with...

Good points! * I think warnings are a lot more user-friendly than errors ("Lean knows what I mean, why doesn't it show me the goal state one line below the...