Doc improvements

doc/create_game.md

@@ -194,7 +194,7 @@ You can but a `Statement` inside namespaces like you would with `theorem`.
 
 #### Doc String / Exercise statement
 
-Add a docstring that contains the exercise statement in natural language. If you do this, it will appear at the top of the exercise. It supports Latex.
+Add a docstring that contains the exercise statement in natural language. If you do this, it will appear at the top of the exercise. It supports KateX.
 
 ```lean
 /-- The exercise statement in natural language using latex: $\iff$. -/
@@ -265,13 +265,11 @@ CoverImage "images/cover.png"
 * `Prerequisites` a list of other games you should play before this one, e.g. `Prerequisites "NNG" "STG"`. The game names are free-text.
 * `CoverImage`: You can create a folder `images/` and put images there for the game to use. The maximal ratio is ca. 500x200 (W x H) but it might be cropped horizontally on narrow screens.
 
-## Further Notes
+## 10. Advanced Topics
+### Number Of Levels Limit
+A world with more than 16 levels will be displayed with the levels spiraling outwards,
+it might be desirable to stay below that bound. Above 22 levels the spiral starts getting out
+of control.
 
-Here are some random further things you should consider designing a new game:
-
-* Inside strings, you need to escape backslashes, but not inside doc-strings, therefore you
-  would write `Introduction "some latex here: $\\iff$."` but
-  `/-- some latex here: $\iff$. -/ Statement ...`
-* A world with more than 16 levels will be displayed with the levels spiraling outwards,
-  it might be desirable to stay below that bound. Above 22 levels the spiral starts getting out
-  of control.
+### Latex support
+See latex.md

doc/hints.md

@@ -82,16 +82,7 @@ You should probably use `(strict := true)` if you want to give fine-grained deta
 tactics like `have` which do not modify the goal or any existing assumptions, but only
 create new assumptions.
 
-## 6. Formatting
 
-You can add use markdown to format your hints, for example you can use KaTex: `$\\iff$`
-
-**Escaping**: Generally, if you add text inside quotes `" "` (e.g. in `Hint`) you need to escape
-backslashes, but if you provide text inside a doc comment
-`/-- -/` (e.g. in the `Statement` description) you do not!
-Further, inside `Hint` you need to escape all opening curly brackets as `\{` since `{h}` is syntax for inserting a variable name `h`.
-
-TODO: Write a doc about latex/markdown options available.
 
 ### Commutative diagrams
 
@@ -120,3 +111,19 @@ $$
 ```
 
 See https://www.jmilne.org/not/Mamscd.pdf
+
+### Truth Tables
+KateX does not support the tabular environment. You can use the array environment instead.
+```
+$$
+\\begin{array}{|c|c|} 
+\\hline
+P & ¬P \\\\
+\\hline
+T & F  \\\\
+F & T  \\\\
+\\hline
+\\end{array}
+$$
+```
+

doc/latex.md

@@ -0,0 +1,15 @@
+# Escaping
+Generally, if you add text inside quotes `" "` (e.g. in `Hint`) you need to escape
+backslashes, but if you provide text inside a doc comment
+`/-- -/` (e.g. in the `Statement` description) you do not!
+
+Furthermore, inside `Hint` you need to escape all opening curly brackets as `\{` since `{h}` is syntax for inserting a variable name `h`.
+
+## Example
+Inside strings, you need to escape backslashes, but not inside doc-strings, therefore you
+  would write `Introduction "some latex here: $\\iff$."` ,  but
+  `/-- some latex here: $\iff$. -/ Statement ...`
+
+# Support
+It is important to mention that KateX supports most but not all of latex and its packages.
+See [supported](https://katex.org/docs/supported.html).

doc/writing_exercises.md

@@ -54,3 +54,8 @@ You can add attributes as you would for a `theorem`. Most notably, you can make
 @[simp]
 Statement my_simp_lemma ...
 ```
+
+## Formatting
+
+You can use markdown to format inside quotes like `Hint ""`.
+Latex is also supported, see latex.md.