trying to centralize information

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
 

doc/latex.md

@@ -1,8 +1,19 @@
-# Syntax
+# 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
+  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.