From adb93e30bd0c0364a91b7ee4c606a01d33c5acd4 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 7 Aug 2023 12:54:22 +0200 Subject: [PATCH] update documentation --- DOCUMENTATION.md | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/DOCUMENTATION.md b/DOCUMENTATION.md index 07eae5c..4b1e21c 100644 --- a/DOCUMENTATION.md +++ b/DOCUMENTATION.md @@ -188,6 +188,27 @@ can define which tab is open when the level is loaded by adding `LemmaTab "Pow"` There will be features added to get automatic information from mathlib! +## Escaping +(TODO: Move) + + +Inside the doc comment you don't need to escape the backslashes: + +``` +/-- $\operatorname{succ}(n)$. notation for naturals is `\N`. -/ +Statement ... +``` + +However, inside interpolated strings (e.g. in `Hint`, `Introduction` and `Conclusion`) +you do need to escape backslashes +with `\\` and `{` with `\{`: + +``` +Hint "This code has some $\\operatorname\{succ}(n)$ math. The value of `h` is {h}. +Notation for naturals is `\\N`." +``` + + # Running Games Locally The installation instructions are not yet tested on Mac/Windows. Comments very welcome!