Zulip Chat Archive
Stream: Lean for teaching
Topic: English (tag)
Martin Dvořák (Feb 27 2026 at 14:24):
Do we want to delete the tag "English" here?
https://leanprover-community.github.io/teaching/courses.html
Or do we want to put it on all courses in English?
Martin Dvořák (Feb 27 2026 at 14:26):
Also there is "portuguese" and "Portuguese" but they filter the same three items.
Last updated: Feb 28 2026 at 14:05 UTC