Improve texts

2023-03-03 17:00:05 +01:00
parent a42841ba97
commit 5af93f0a2a
3 changed files with 8 additions and 9 deletions
@@ -12,18 +12,17 @@ Introduction
 Willkommen zum Lean-Crashkurs wo du lernst wie man mathematische Beweise vom Computer
 unterstützt und verifiziert schreiben kann.

-*Rechts* siehst den Status des Beweis. Unter **Main Goal** steht, was du im Moment am beweisen
-bist. Falls es mehrere Subgoals gibt, werden alle weiteren darunter unter **Further Goals**
+In der *mittleren Spalte* siehst den Status des Beweis. Unter **Main Goal** steht, was du im Moment
+beweisen musst. Falls es mehrere Dinge zu beweisen gibt, werden alle weiteren darunter unter **Further Goals**
 aufgelistet, diese musst du dann später auch noch zeigen.

 Ein Beweis besteht aus mehreren **Taktiken**. Das sind einzelne Beweisschritte, ähnlich wie
 man auf Papier argumentieren würde. Manche Taktiken können ganz konkret etwas kleines machen,
-andere sind stark und lösen ganze Probleme automatisiert. Du findest die Taktiken *Links* an der
-Seite.
+andere sind stark und lösen ganze Probleme automatisiert. Du findest die Taktiken in der *rechten Spalte*.

 Wenn der Beweis komplett ist, erscheint \"Level completed! 🎉\".

-Als erstes ein kleiner Preview, dass Lean auch vieles automatisch kann. So gibt es eine
+Als erste kleine Vorschau, dass Lean auch vieles automatisch kann, gibt es eine
 Taktik `tauto`, die alle wahren Aussagen der Prädikaten-Logik beweisen kann.

 Dieses Beispiel würde von Hand etwas Zeit in Anspruch nehmen. Lean ist da viel schneller.
@@ -44,7 +43,7 @@ $$
  tauto

 Hint (A B C : Prop): ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) =>
-"Man schreibt eine Taktik pro Zeile, also gib `tauto` ein und geh mit Enter ⏎ auf eine neue Zeile."
+"Gib `tauto` ein und drücke Enter ⏎."

 Conclusion ""

@@ -11,7 +11,7 @@ Introduction
 Jetzt gehen wir aber einen Schritt zurück und lernen, wie man konkret mit Lean arbeitet,
 damit du verstehst, was `tauto` hinter der Kulisse macht.

-Deine erste Taktik ist `rfl` (für \"reflexivity\"), welche dazu da ist,
+Eine der grundlegendsten Taktiken ist `rfl` (für \"reflexivity\"), welche dazu da ist,
 ein Goal der Form $X = X$ zu schließen.
 "

@@ -23,7 +23,7 @@ Statement
 -- "Die Taktik `rfl` beweist ein Goal der Form `X = X`."

 HiddenHint : 42 = 42 =>
-"Man schreibt eine Taktik pro Zeile, also gib `rfl` ein und geh mit Enter ⏎ auf eine neue Zeile."
+"Die beiden Seiten dieser Gleichung sind identisch, also gib `rfl` ein und drücke Enter ⏎"

 Conclusion "Bravo! PS: `rfl` steht für \"reflexivity\"."

@@ -22,7 +22,7 @@ Wenn das Goal genau einer Annahme entspricht, kann man diese mit `assumption` be
 "

 Statement
-"Angenommen $1 < n$. dann ist $1 < n$."
+"Angenommen $1 < n$. Dann ist $1 < n$."
    (n : ℕ) (h : 1 < n) : 1 < n := by
  assumption