Merge pull request #10 from mcol/typos

Fix typos.

Game/Doc/Lemmas.lean

@@ -8,7 +8,7 @@ def and_left {P Q : Prop} (h : P ∧ Q) : P := And.left h
 # ∧ Elimination Left
 ### `and_left : P ∧ Q -> P`
 
-If `h` is a term with a type like `AP∧ Q`
+If `h` is a term with a type like `P ∧ Q`
 
 `and_left h`, `h.left` or `h.1` are all expressions for denoting the left-hand side of the given evidence. In this case, the left side has a type of `P`.
 -/
@@ -104,7 +104,7 @@ def or_elim
 
 /--
 # Or Elimination
-If you can conclude something from `A` and you can conclude the same thing from `B`, then if you know `A ∨ B` it won't matter which of the two happens as you can still guarentee something.
+If you can conclude something from `A` and you can conclude the same thing from `B`, then if you know `A ∨ B` it won't matter which of the two happens as you can still guarantee something.
 
 or_elim is also evidence:
 ```
@@ -116,7 +116,7 @@ or_elim : (P ∨ Q) → (P → R) → (Q → R) → R`
 2. evidence an implication on the left,
 3. evidence for an implication on the right.
 # Example
-`or_elim` is your first 3-paramater function.
+`or_elim` is your first 3-parameter function.
 ```
 pvq: P ∨ Q
 pr : P → R
@@ -202,7 +202,7 @@ There is are infix operators for function application; they look like `|>` and `
 
 It's twin, `|>` chains such that `x |> f |> g` is interpreted as `g (f x)`.
 
-What makes the infix operators usefull is that they can often replace a pair of brackets `(...)` making expressions easier to read.
+What makes the infix operators useful is that they can often replace a pair of brackets `(...)` making expressions easier to read.
 
 ----
 # Computer Science

Game/Doc/Tactics.lean

@@ -2,7 +2,7 @@ import GameServer.Commands
 
 /--
 # Summary
-The `exact` tactic is a means through which you give the game your answer. Many levels can be done in multiple steps. You'll use the `exact` tactic when you're ready to create the final expression. It will be evaluated to see weather it matches the goal.
+The `exact` tactic is a means through which you give the game your answer. Many levels can be done in multiple steps. You'll use the `exact` tactic when you're ready to create the final expression. It will be evaluated to see whether it matches the goal.
 
 `exact` will work with any expression and attempt to unify it with the current goal. The simplest such expression is just a name that — `:` — “is evidence for” the goal. More complicated expressions often make use of unlocked definitions and theorems as well as function abstraction and application.
 

Game/Levels/AndIntro/L02.lean

@@ -33,7 +33,7 @@ Use `p` and `s` to produce evidence that `P ∧ S`. Remember that you use eviden
 # Using the `∧` Construtor
 This level has unlocked “`∧`” under definitions. This has made the `and_intro` theorem available. You can use `and_intro` by giving it the two relevant pieces of evidence. The expression looks like: `and_intro e₁ e₂` where `e₁` and `e₂` are evidence.\\
 \\
-The help-page has even more detail about creating conjunctions like this (There's a common shorthand using angle-brackers `⟨` `,` `⟩` ).
+The help page has even more detail about creating conjunctions like this (There's a common shorthand using angle-brackets `⟨` `,` `⟩` ).
 
 # A reminder
 Use the `exact` tactic to exhibit evidence for a goal

Game/Levels/AndTactic/L05.lean

@@ -12,7 +12,7 @@ OnlyTactic
 
 Introduction "
 # Rinse and Repeat
-When you were writing expressions before, lvl 4 needed `and_left` while level 5 needed `and_right`. Tactics can incorperate an arbitrary amount of automation. In this case, because assumption will do a search through your assumptions for you, your proof for this level can be 100% identical to the one you used last level.
+When you were writing expressions before, level 4 needed `and_left` while level 5 needed `and_right`. Tactics can incorporate an arbitrary amount of automation. In this case, because `assumption` will do a search through your assumptions for you, your proof for this level can be 100% identical to the one you used in the last level.
 "
 
 /-- Both P and Q entails just Q as well! -/

Game/Levels/IffIntro/L01.lean

@@ -14,7 +14,7 @@ OnlyTactic
 
 Introduction "
 # Coupled Conditionals
-Sybeth and Alarfil are a couple. In effect, this means that if Sybeth is playing a party game, then Alarfil is playing too and vise versa. Therefore Sybeth is playing Charades if and only if Alarfil playing.
+Sybeth and Alarfil are a couple. In effect, this means that if Sybeth is playing a party game, then Alarfil is playing too and vice versa. Therefore Sybeth is playing Charades if and only if Alarfil playing.
 # Proposition Key:
 - J — Alarfil is playing Charades
 - S — Sybeth is playing Charades

Game/Levels/IffIntro/L02.lean

@@ -4,7 +4,7 @@ open GameLogic
 
 World "IffIntro"
 Level 2
-Title "Conjuctive Iff"
+Title "Conjunctive Iff"
 
 NewTheorem
   GameLogic.iff_mp

Game/Levels/IffIntro/L07.lean

@@ -14,7 +14,7 @@ Introduction "
 # BOSS LEVEL
 This is an involved level. It doesn't require you to do anything tricky, but there are a lot of moving parts and it is easy to lose track of what you're doing.\\
 \\
-I recommend editor mode. Think about what this is asking you to prove and use `have` to give yourself any auxillary facts that don't exist under your theorems.
+I recommend editor mode. Think about what this is asking you to prove and use `have` to give yourself any auxiliary facts that don't exist under your theorems.
 "
 
 Statement (P Q R : Prop): (P ∧ Q ↔ R ∧ Q) ↔ Q → (P ↔ R) := by

Game/Levels/IffTactic/L02.lean

@@ -4,7 +4,7 @@ open GameLogic
 
 World "IffTactic"
 Level 2
-Title "Conjuctive Iff"
+Title "Conjunctive Iff"
 
 OnlyTactic
   assumption

Game/Levels/IffTactic/L05.lean

@@ -19,7 +19,7 @@ OnlyTactic
 
 Introduction "
 # A Longer Level
-The `rw` tactic makes this level a cakewalk. For the redux version we're going to make this outright tedius, but this will show without a doubt that you've mastered simple propositional proofs.\\
+The `rw` tactic makes this level a cakewalk. For the redux version we're going to make this outright tedious, but this will show without a doubt that you've mastered simple propositional proofs.\\
 \\
 I suggest you finish the other redux worlds before doing this level.\\
 \\

Game/Levels/ImpIntro.lean

@@ -22,7 +22,7 @@ This game uses the implication arrow “ → ”. “If A, then B” is the same
 \\
 So far, we've been giving our evidence and propositions real-world analogues. Doing this is a bit less desirable with conditionals as real-world evidence is often based on our understanding and not some tangible object. For example; the evidence that “If it rained, then the driveway is wet” generally doesn't come in the form of peer-reviewed physics papers. You should be thinking of the flavour text for each level as an unrefined embellishment of the symbols you're actually concerned with.\\
 \\
-That said, at the level the favour text works on, what would constitute evidence for a conditional statement? Well, for example; “If we have gnocchi, butter, parmesan, and black pepper, then we can cook *gnocchi cacio e pepe*”. An example of evidence for such a conditional could be a recipe with cooking instructions. You can think of the recipe as an argument explaining that the given ingredients are sufficient to be able to cook the dish.\\
+That said, at the level the flavour text works on, what would constitute evidence for a conditional statement? Well, for example; “If we have gnocchi, butter, parmesan, and black pepper, then we can cook *gnocchi cacio e pepe*”. An example of evidence for such a conditional could be a recipe with cooking instructions. You can think of the recipe as an argument explaining that the given ingredients are sufficient to be able to cook the dish.\\
 \\
 Another example might be a safe's combination, as evidence that “I can find the hidden safe” → “I can steal the contents of the safe”. Perhaps a certification is evidence that “I won the contract” → “I will renovate the client's yard”.\\
 \\

Game/Levels/ImpIntro/L08.lean

@@ -31,5 +31,5 @@ example (C D S : Prop) (h : (S → C) ∧ (S → D)) : S → C ∧ D := by
   exact λs ↦ ⟨l s, r s⟩
 
 Conclusion "
-You definitely have the knack of providing conditional arguements
+You definitely have a knack for providing conditional arguments!
 "

Game/Levels/ImpIntro/L09.lean

@@ -26,7 +26,7 @@ That's a bit convoluted, but you should be able to produce some evidence of this
 - `S` — Sybeth is bringing a snack
 "
 
-/-- Write the nessesary nested function(s)! -/
+/-- Write the necessary nested function(s)! -/
 Statement (R S : Prop) : R → (S → R) ∧ (¬S → R) := by
   exact λ(r : R) ↦ and_intro (λ(_ : S) ↦ r) (λ(_ : ¬S) ↦ r)
 

Game/Levels/NotIntro/L02.lean

@@ -22,9 +22,9 @@ You've unlocked the \"false implies anything\" function. `false_elim` will take
 # A Tip
 Remember you can think of `h : ¬S` as `h : S → False`.\\
 \\
-Once you've started with `λ(s : S) ↦ `, you'll then see that the expression `h s` evaluates to evidence for `False`. If ever you have evidence for `False`, you should aways immediatly consider using `false_elim` to create evidence for anything — which in this case will be `B`.\\
+Once you've started with `λ(s : S) ↦ `, you'll then see that the expression `h s` evaluates to evidence for `False`. If ever you have evidence for `False`, you should always immediately consider using `false_elim` to create evidence for anything — which in this case will be `B`.\\
 \\
-There is no proof that \"keeps going\" once you've created evidence for `False`. Some proofs have multiple parts, so you may close off one line of reasoning and move on to another, but there can be no meaningfull logic in any context where evidence for `False` is present.
+There is no proof that \"keeps going\" once you've created evidence for `False`. Some proofs have multiple parts, so you may close off one line of reasoning and move on to another, but there can be no meaningful logic in any context where evidence for `False` is present.
 "
 
 /-- ¬S is enough to show S → B -/

Game/Levels/NotIntro/L05.lean

@@ -23,7 +23,7 @@ Statement (B S : Prop)(h1 : B → S)(h2 : ¬S) : ¬B := by
   exact imp_trans h1 h2
 
 Conclusion "
-Congradulations. Did you recognise this proof? It's actually a slightly less general version of the proof you used in the \"**→ Tutotial world, level 4**\" to show that implication is transitive.
+Congratulations. Did you recognise this proof? It's actually a slightly less general version of the proof you used in the \"**→ Tutotial world, level 4**\" to show that implication is transitive.
 
 ---
 Thinking of `h₂` as `Q → False`, you can actually use your imp_trans theorem here.

Game/Levels/NotIntro/L08.lean

@@ -18,7 +18,7 @@ Your cake order definitely has sprinkles, which means it's **not** missing sprin
 - `S` — The cake is topped with sprinkles
 "
 
-/-- Negation into conjuction. -/
+/-- Negation into conjunction. -/
 Statement (C S : Prop) (s: S) : ¬(¬S ∧ C) := by
   exact λ(nsc : ¬S ∧ C) ↦ nsc.left s
 

Game/Levels/NotIntro/L09.lean

@@ -12,9 +12,9 @@ OnlyTactic
 
 Introduction "
 # Allergy #1
-Owing to his allergy, if Pippin is present, there must be no avocado at the party. Which means that we cannot have both Pippin and avacado at the party
+Owing to his allergy, if Pippin is present, there must be no avocado at the party. Which means that we cannot have both Pippin and avocado at the party
 # Proposition Key:
-- `A` — There's avacado at the party
+- `A` — There's avocado at the party
 - `P` — Pippin is attending the party
 "
 

Game/Levels/NotIntro/L10.lean

@@ -4,17 +4,17 @@ open GameLogic
 
 World "NotIntro"
 Level 10
-Title "Conjunction Implicaiton"
+Title "Conjunction Implication"
 
 OnlyTactic
   exact
   «have»
 
 Introduction "
 # Allergy #2
-We cannot have both Pippin and avacado at the party. Which means that if Pippin is attending, then there will not be any avacado.
+We cannot have both Pippin and avocado at the party. Which means that if Pippin is attending, then there will not be any avocado.
 # Proposition Key:
-- `A` — There's avacado at the party
+- `A` — There's avocado at the party
 - `P` — Pippin is attending the party
 "
 

Game/Levels/NotIntro/L11.lean

@@ -12,9 +12,9 @@ OnlyTactic
 
 Introduction "
 # Allergy: Triple Confusion
-Pippin is allergic to avocado. You tell him you're not *not* **not** bringing avacado!!! Pippin gives you a confused look, but after a moment of contemplation, he responds with, \"Ok, good to know.\"
+Pippin is allergic to avocado. You tell him you're not *not* **not** bringing avocado!!! Pippin gives you a confused look, but after a moment of contemplation, he responds with, \"Ok, good to know.\"
 # Proposition Key:
-- `A` — You're bringing avacado
+- `A` — You're bringing avocado
 "
 
 /-- ¬A is stable. -/

Game/Levels/NotIntro/L12.lean

@@ -29,7 +29,7 @@ example (B C : Prop) (h : ¬(B → C)) : ¬¬B := by
   exact λnb ↦ h (nb ≫ false_elim)
 
 Conclusion "
-These unintuitive statements highlight the inherent challenge in contemplating the *potential* existence (or definite non-existance) of implications.
+These unintuitive statements highlight the inherent challenge in contemplating the *potential* existence (or definite non-existence) of implications.
 
 That's a twist of logic, to be sure!
 "

Game/Levels/NotTactic/L02.lean

@@ -12,7 +12,7 @@ OnlyTactic
   contradiction
 
 Introduction "
-# Contradiciton
+# Contradiction
 This level introduces a relatively powerful tactic. Contradiction is a finishing tactic that will look through your assumptions and discharge some of the more obvious contradictions in order to solve any goal.\\
 \\
 examples:

Game/Levels/NotTactic/L03.lean

@@ -15,7 +15,7 @@ OnlyTactic
 
 Introduction "
 # exfalso
-`exfalso` is **Contradiction**'s younger brother. Using `exfalso` turns your goal to `False`. This is the same thing as using `apply false_elim`. Using the principle that “from nonsense, follows nonsense,” if you spot a constradiction in your assumptions, you can make progress by changing your goal to `False.`\\
+`exfalso` is **Contradiction**'s younger brother. Using `exfalso` turns your goal to `False`. This is the same thing as using `apply false_elim`. Using the principle that “from nonsense, follows nonsense,” if you spot a contradiction in your assumptions, you can make progress by changing your goal to `False.`\\
 \\
 Remember that because `¬P` is the same as `P → False`, you can use the `apply` tactic on evidence for `¬P`
 "

Game/Levels/NotTactic/L08.lean

@@ -17,7 +17,7 @@ Introduction "
 You can solve this level using the knowledge you've aquired so far. If you've used a language with destructuring or pattern matching before, then you can introduce and pattern-match in one step with `intro ⟨nq, p⟩`. Doing so means you won't need the `cases` tactic for this level.
 "
 
-/-- Negation into conjuction. -/
+/-- Negation into conjunction. -/
 Statement (P Q : Prop) (h: Q) : ¬(¬Q ∧ P) := by
   intro nqp
   cases nqp

Game/Levels/NotTactic/L10.lean

@@ -4,7 +4,7 @@ open GameLogic
 
 World "NotTactic"
 Level 10
-Title "Conjunction Implicaiton"
+Title "Conjunction Implication"
 
 OnlyTactic
   assumption

Game/Levels/OrIntro/L02.lean

@@ -28,7 +28,7 @@ Statement (O S : Prop)(s : S) : K ∨ S := by
 Conclusion "
 Almost a repeat of level 1. That was fast.
 
-You'll notice that last time you showed evidence for a proposition involving “Oranges are a vegetable” even though you probably know that oranges are a fruit and not a vegitable. This time you did the same for “sprinkles are super colourful,” which you probably know is true.
+You'll notice that last time you showed evidence for a proposition involving “Oranges are a vegetable” even though you probably know that oranges are a fruit and not a vegetable. This time you did the same for “sprinkles are super colourful,” which you probably know is true.
 
 What this demonstrates is that `∨` is an inclusive “or”, which means at least one of the propositions is true. It could be both or just one.
 "

Game/Levels/OrIntro/L03.lean

@@ -19,14 +19,14 @@ Here's the deal. Ilyn and Cyna both said they're bringing board games and you're
 - `C` — Cyna is coming to the party
 - `I` — Ilyn is coming to the party
 # Or Elimination
-If you can conclude something from `A` and you can conclude the same thing from `B`, then if you know `A ∨ B` it won't matter which of the two happens as you can still guarentee something.
+If you can conclude something from `A` and you can conclude the same thing from `B`, then if you know `A ∨ B` it won't matter which of the two happens as you can still guarantee something.
 # You've unlocked `or_elim`
 `or_elim` has three parameters:
 1. takes evidence for a disjunction,
 2. evidence an implication on the left,
 3. evidence for an implication on the right.
 
-`or_elim` is your first 3-paramater function. The associated proposition is `or_elim : (P ∨ Q) → (P → R) → (Q → R) → R`.
+`or_elim` is your first 3-parameter function. The associated proposition is `or_elim : (P ∨ Q) → (P → R) → (Q → R) → R`.
 ```
 pvq: P ∨ Q
 pr : P → R

Game/Levels/OrIntro/L05.lean

@@ -16,7 +16,7 @@ Introduction "
 If the cake arrives, then everybody will rejoice. Either the cake arrives or you get a refund. Therefore, either everybody will rejoice or you get a refund! That's a win-win situation.
 # Proposition Key:
 - C — The cake arrives
-- J — Everybody is joyfull
+- J — Everybody is joyful
 - R — You get a refund
 "