fix typo

doc/writing_exercises.md

@@ -26,23 +26,23 @@ f: ℤ → ℤ := fun x => 2 * x
 ⊢ 0 < f a
 ```
 
-## "Preample" & non-`Prop`-valued exercises
+## "Preamble" & non-`Prop`-valued exercises
 
-You can use the following syntax with `(preample := tac)` where `tac` is a tactic sequence.
+You can use the following syntax with `(preamble := tac)` where `tac` is a tactic sequence.
 
 ```
-Statement my_statement (preample := dsimp) (a : ℤ) (h : 0 < a) :
+Statement my_statement (preamble := dsimp) (a : ℤ) (h : 0 < a) :
     0 < f a := by
   sorry
 ```
 
 This tactic sequence will be executed before the exercise is handed to the player.
 
-For example, if your exercise is to construct a structure, you could use `preample` to fill
+For example, if your exercise is to construct a structure, you could use `preamble` to fill
 all data fields correctly, leaving all `Prop`-valued fields of the structure as separate goals
 for the player to proof.
 
-Note: `(preample := tac)` always has to be written between the optional name and the first
+Note: `(preamble := tac)` always has to be written between the optional name and the first
 hypothesis. Nevertheless, you can use all hypotheses in the tactic sequence, because it is
 only evaluated at the beginning of the proof.
 

server/GameServer/Commands.lean

@@ -345,7 +345,7 @@ elab "LemmaTab"  category:str : command => do
 
 /-! # Exercise Statement -/
 
-/-- You can write `Statement add_comm (preample := simp) .... := by` which
+/-- You can write `Statement add_comm (preamble := simp) .... := by` which
 will automatically execute the given tactic sequence before the exercise
 is handed to the player.
 
@@ -361,18 +361,18 @@ For example in "Show that all matrices with first column zero form a submodule",
 you could provide the set of all these matrices as `carrier` and the player will receive
 all the `Prop`-valued fields as goals.
 -/
-syntax preampleArg := atomic(" (preample := " withoutPosition(tacticSeq) ")")
+syntax preambleArg := atomic(" (preamble := " withoutPosition(tacticSeq) ")")
 
 /-- Define the statement of the current level. -/
 elab doc:docComment ? attrs:Parser.Term.attributes ?
-    "Statement" statementName:ident ? preample:preampleArg ? sig:declSig val:declVal : command => do
+    "Statement" statementName:ident ? preamble:preambleArg ? sig:declSig val:declVal : command => do
   let lvlIdx ← getCurLevelIdx
 
   -- add an optional tactic sequence that the engine executes before the game starts
-  let preampleSeq : TSyntax `Lean.Parser.Tactic.tacticSeq ← match preample with
+  let preambleSeq : TSyntax `Lean.Parser.Tactic.tacticSeq ← match preamble with
   | none => `(Parser.Tactic.tacticSeq|skip)
   | some x => match x with
-    | `(preampleArg| (preample := $tac)) => pure tac
+    | `(preambleArg| (preamble := $tac)) => pure tac
     | _ => `(Parser.Tactic.tacticSeq|skip)
 
   let docContent ← parseDocComment doc
@@ -414,17 +414,17 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
       -- in that case.
       logWarningAt name (m!"Environment already contains {fullName}! Only the existing " ++
       m!"statement will be available in later levels:\n\n{origType}")
-      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨preampleSeq⟩); $(⟨tacticStx⟩)})
+      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨preambleSeq⟩); $(⟨tacticStx⟩)})
       elabCommand thmStatement
       -- Check that statement has a docs entry.
       checkInventoryDoc .Lemma name (name := fullName) (template := docContent)
     else
-      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig := by {let_intros; $(⟨preampleSeq⟩); $(⟨tacticStx⟩)})
+      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig := by {let_intros; $(⟨preambleSeq⟩); $(⟨tacticStx⟩)})
       elabCommand thmStatement
       -- Check that statement has a docs entry.
       checkInventoryDoc .Lemma name (name := fullName) (template := docContent)
   | none =>
-    let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨preampleSeq⟩); $(⟨tacticStx⟩)})
+    let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨preambleSeq⟩); $(⟨tacticStx⟩)})
     elabCommand thmStatement
 
   let msgs := (← get).messages
@@ -499,7 +499,7 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
   modifyCurLevel fun level => pure { level with
     module := env.header.mainModule
     goal := sig,
-    preample := preampleSeq
+    preamble := preambleSeq
     scope := scope,
     descrText := docContent
     statementName := match statementName with

server/GameServer/EnvExtensions.lean

@@ -266,7 +266,7 @@ structure GameLevel where
   /-- The image for this level. -/
   image : String := default
   /-- A sequence of tactics the game automatically executes before the first step. -/
-  preample : TSyntax `Lean.Parser.Tactic.tacticSeq := default
+  preamble : TSyntax `Lean.Parser.Tactic.tacticSeq := default
 deriving Inhabited, Repr
 
 /-- Json-encodable version of `GameLevel`

server/GameServer/FileWorker.lean

@@ -263,7 +263,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           -- This makes the experience for the user much nicer and allows for local
           -- definitions in the exercise.
           let cmdStx ← `(command|
-            theorem the_theorem $(level.goal) := by {let_intros; $(⟨level.preample⟩); $(⟨tacticStx⟩)} )
+            theorem the_theorem $(level.goal) := by {let_intros; $(⟨level.preamble⟩); $(⟨tacticStx⟩)} )
           Elab.Command.elabCommandTopLevel cmdStx)
       cmdCtx cmdStateRef
   let postNew := (← tacticCacheNew.get).post

server/test/test_statement.lean

@@ -81,5 +81,5 @@ example (n m : Nat) : (m + n) + x = m + (n + x) := by
 
 #check My.add_assoc
 
-Statement My.add_comm (preample := simp [add_comm m n]) (n m : Nat) : n + (m + 0) = m + n := by
+Statement My.add_comm (preamble := simp [add_comm m n]) (n m : Nat) : n + (m + 0) = m + n := by
   rw [Nat.add_comm]