From 8a61ad6e5d5277495c8319fb96b42ca32c2cf2ff Mon Sep 17 00:00:00 2001
From: Jad <jad-abou-hawili@hotmail.com>
Date: Sat, 13 Jul 2024 20:58:08 +0300
Subject: [PATCH] trying to centralize information

---
 doc/hints.md             |  9 ---------
 doc/latex.md             | 15 +++++++++++++--
 doc/writing_exercises.md |  5 +++++
 3 files changed, 18 insertions(+), 11 deletions(-)

diff --git a/doc/hints.md b/doc/hints.md
index bc1f299..cb88550 100644
--- a/doc/hints.md
+++ b/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
 
diff --git a/doc/latex.md b/doc/latex.md
index cb191a4..5e892dd 100644
--- a/doc/latex.md
+++ b/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).
+
+
+
+
diff --git a/doc/writing_exercises.md b/doc/writing_exercises.md
index 8d8483e..c3d85c5 100644
--- a/doc/writing_exercises.md
+++ b/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.