@@ -468,6 +468,23 @@ msgstr ""
468468msgid "Conjunction §0 is \" and\" . Use §1 to use it, §2 to prove it."
469469msgstr ""
470470
471+ #: Game
472+ msgid "# Glimpse of Lean\n"
473+ "\n"
474+ "Welcome to this tutorial designed to give you a glimpse of Lean.\n"
475+ "\n"
476+ "This game is split into **Worlds**. Each world focuses on a specific aspect of Lean.\n"
477+ "\n"
478+ "* **Computing**: Learn how to calculate and rewrite equalities (Basic & Advanced).\n"
479+ "* **Logic**: Learn how to handle logical implications, equivalences, quantifiers, and conjunctions (Parts 1-3).\n"
480+ "* **Analysis**: Learn how to handle limits of sequences.\n"
481+ "* **Set Theory**: Explore Galois connections and lattices.\n"
482+ "* **Algebra**: Explore rings, homomorphisms, and ideals.\n"
483+ "* **Probability**: Explore probability measures and independence.\n"
484+ "\n"
485+ "Start with the **Computing (1)** world to learn the basics."
486+ msgstr ""
487+
471488#. §0: `A`
472489#. §1: `B`
473490#. §2: `ℙ (A ∩ B) = ℙ A * ℙ B`
@@ -488,23 +505,6 @@ msgid "We can also use lemmas from the library. For instance §0 proves\n"
488505"§1. We will rewrite twice with this lemma."
489506msgstr ""
490507
491- #: Game
492- msgid "# Glimpse of Lean\n"
493- "\n"
494- "Welcome to this tutorial designed to give you a glimpse of Lean.\n"
495- "\n"
496- "This game is split into **Worlds**. Each world focuses on a specific aspect of Lean.\n"
497- "\n"
498- "* **Computing**: Learn how to calculate and rewrite equalities.\n"
499- "* **Logic**: Learn how to handle logical implications and quantifiers.\n"
500- "* **Analysis**: Learn how to handle limits of sequences.\n"
501- "* **Set Theory**: Explore Galois connections and lattices.\n"
502- "* **Algebra**: Explore rings, homomorphisms, and ideals.\n"
503- "* **Probability**: Explore probability measures and independence.\n"
504- "\n"
505- "Start with the **Computing** world to learn the basics."
506- msgstr ""
507-
508508#: Game.Levels.Logic.L08_EquivRw
509509msgid "Equivalences allow rewriting in both directions."
510510msgstr ""
0 commit comments