From 2e4161ca7aa1b8b0ebfee6908718cdc706bd4e16 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 30 Mar 2023 17:48:55 +0200 Subject: [PATCH] typos --- server/adam/Adam/Levels/Contradiction/L02_Suffices.lean | 3 +-- server/adam/Adam/Levels/Implication/L01_Intro.lean | 8 ++++---- server/adam/Adam/Levels/Implication/L06_Iff.lean | 4 ++-- server/adam/Adam/Levels/Predicate/L02_Rewrite.lean | 4 +++- 4 files changed, 10 insertions(+), 9 deletions(-) diff --git a/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean b/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean index bb954b7..270402c 100644 --- a/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean +++ b/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean @@ -55,5 +55,4 @@ Statement NewTactic «suffices» DisabledTactic «have» -Conclusion "**Benedictus**: Genau so meinte ich das. Ob Ihr nun in Zukunft `have` und `suffices` verwendet, ist reine Geschmacksfrage. Hauptsache, Ihr wisst, wie Ihr entfernte Ziele in kleinen Schritte erreicht. - +Conclusion "**Benedictus**: Genau so meinte ich das. Ob Ihr nun in Zukunft `have` und `suffices` verwendet, ist reine Geschmacksfrage. Hauptsache, Ihr wisst, wie Ihr entfernte Ziele in kleinen Schritte erreicht." diff --git a/server/adam/Adam/Levels/Implication/L01_Intro.lean b/server/adam/Adam/Levels/Implication/L01_Intro.lean index 5bac3e2..b215b37 100644 --- a/server/adam/Adam/Levels/Implication/L01_Intro.lean +++ b/server/adam/Adam/Levels/Implication/L01_Intro.lean @@ -16,11 +16,11 @@ Introduction Statement (A B : Prop) (hb : B) : A → (A ∧ B) := by Hint " - **Operationsleiter:** Die Arbeiten meinen, das wäre so richtig und wir würden das dringend brauchen. Aber keiner kann es mir beweisen. + **Operationsleiter:** Die Arbeiten meinen, das wäre so richtig und wir würden das dringend brauchen. Aber keiner kann es mir beweisen. **Du**: Einen Moment. Das ist ja gerade so eine Implikation (`\\to`). Wir nehmen an, dass `{B}` gilt, und wollen zeigen, dass dann gilt `{A}` impliziert `{A} und {B}`. Ja, klar! Natürlich stimmt das. - Der Operationsleiter sieht Dich erwartungsvoll an. + Der Operationsleiter sieht Dich erwartungsvoll an. **Du** *(leise zu Robo)*: Soll ich ihm `tauto` aufschreiben? @@ -29,7 +29,7 @@ Statement (A B : Prop) (hb : B) : A → (A ∧ B) := by *Du**: Aber wie denn? Ich glaube, ich würde als erstes gern so etwas sagen wie 'Nehmen wir also an, `{A}` gilt …' - **Robo**: Ja, gute Idee. Wähle dazu für Deine Annahme einfach einen Namen, zum Beispiel `{h}`, und schreib `intro {h}`." + **Robo**: Ja, gute Idee. Wähle dazu für Deine Annahme einfach einen Namen, zum Beispiel `h`, und schreib `intro h`." intro hA Hint "**Du**: OK. Jetzt habe ich also sowohl `{A}` als auch `{B}` in meinen Annahmen und muss `{A} ∧ {B}` zeigen. @@ -42,7 +42,7 @@ Conclusion "**Operationsleiter:** Perfekt! Danke schön! Er geht zu einer Schalttafel und ein paar Knöpfe. Irgendwo setzt sich lautstark ein Förderband in Bewegung. -**Operationsleiter:** Habt Ihr vielleicht noch ein paar Minuten? +**Operationsleiter:** Habt Ihr vielleicht noch ein paar Minuten? " NewTactic intro diff --git a/server/adam/Adam/Levels/Implication/L06_Iff.lean b/server/adam/Adam/Levels/Implication/L06_Iff.lean index e6422e7..fc022f0 100644 --- a/server/adam/Adam/Levels/Implication/L06_Iff.lean +++ b/server/adam/Adam/Levels/Implication/L06_Iff.lean @@ -12,7 +12,7 @@ Introduction " Statement (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by - Hint "**Robo**: `→` ist natürlich Leansch für `$\iff$`. + Hint "**Robo**: `→` ist natürlich Leansch für `$\\iff$`. Die Aussage `A ↔ B` besteht also aus zwei Teilen; sie ist als `⟨A → B, B → A⟩` definiert. **Du**: Also ganz ähnlich wie das UND, `A ∧ B`? @@ -25,7 +25,7 @@ Statement (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by Conclusion " -**Operationsleiter**: Ok, das leuchtet mir ein. +**Operationsleiter**: Ok, das leuchtet mir ein. **Robo** *(zu Dir)*: Übrigens, so wie bei `(h : A ∧ B)` die beiden Teile `h.left` und `h.right` heißen, heißen bei `(h : A ↔ B)` die beiden Teile `h.mp` und `h.mpr`. diff --git a/server/adam/Adam/Levels/Predicate/L02_Rewrite.lean b/server/adam/Adam/Levels/Predicate/L02_Rewrite.lean index 4b0cd4f..ef4bacf 100644 --- a/server/adam/Adam/Levels/Predicate/L02_Rewrite.lean +++ b/server/adam/Adam/Levels/Predicate/L02_Rewrite.lean @@ -14,7 +14,9 @@ Statement (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c : Hint "**Du**: Schau mal, dieses Problem sieht so ähnlich aus wie eines, das wir auf *Implis* schon gelöst hatten. Nur, das hier jetzt Gleichheiten von Zahlen statt Genau-Dann-Wenn-Aussagen stehen! - **Robo**: Richtig. Und im Grunde macht das gar keinen Unterscheid. Du kannst `=` und `↔` praktisch mit `rw` praktisch g"""""leich behandeln." + **Robo**: Richtig. Und im Grunde macht das gar keinen Unterscheid. + Du kannst `=` und `↔` praktisch mit `rw` praktisch gleich behandeln." + Hint (hidden := true) "**Du**: Also auch `rw [hₓ]` und `rw [← hₓ]`? **Robo**: Probiers doch einfach."