search

leanprover-community / leanprover-community.github.io

Hosts the website for mathlib and other Lean community infrastructure.
https://leanprover-community.github.io/
MIT License
53 stars 123 forks source link

It was said that "English" is never mentioned. #432

Closed madvorak closed 8 months ago

eric-wieser commented 9 months ago

@mmasdeu, does this look good to you?

mmasdeu commented 9 months ago

I'm fine with the change. The course was fully in Catalan, but the game is 100% in English so fair to have both tags.

madvorak commented 9 months ago

Well, course in Catalan, even if all materials are in English, qualifies as a course in Catalan.

PatrickMassot commented 9 months ago

I don't see the point of the Catalan tag if all the publicly available files are fully in English. This tag is meant to help people who look for resources in non-English languages and to warn people who are looking for English resources.

mmasdeu commented 9 months ago

I thought that this page was meant as a device to record the different courses that were taking place everywhere. One of its uses is to access the course materials themselves, but there may be other uses. What if some day one wants to say: Lean has been taught at N universities across the globe, in M languages and wants to get the values of N and M from this page?