From 4ad914f171db28ea02785352e27c3147f39dc666 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Thu, 1 Feb 2024 12:22:08 +0100 Subject: [PATCH] Fix a few typos in `user_manual.md` (#3944) --- docs/user_manual.md | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/docs/user_manual.md b/docs/user_manual.md index 9dd057b55a5..5c15f8f48a9 100644 --- a/docs/user_manual.md +++ b/docs/user_manual.md @@ -362,15 +362,15 @@ Here, we have that: `'Hash'Baz'LParUndsCommUndsRParUnds'MYMODULE'Unds'FooBarBaz'Unds'Int'Unds'Int` as the symbol name. -The `symbol` provided *must* be unique to this definition. This is enforced by K. -In general, it's recommended to use `symbol` attribute whenever you use `klabel` -unless you explicitely have a reason not to (eg. you want to *overload* symbols, -or you're using a deprecated backend). It can be very helpful use the `symbol` -attribute for debugging, as many debugging messages are printed in Kast format -which will be more readable with the `symbol` names you explicitely declare. -In addition, if you are programatically manipulating definitions via the JSON -Kast format, building terms using the user-provided pretty -`symbol, klabel(...)` is easier and less error-prone when the auto-generation +The `symbol` provided *must* be unique to this definition. This is enforced by +K. In general, it's recommended to use the `symbol` attribute whenever you use +`klabel` unless you explicitly have a reason not to (eg. you want to *overload* +symbols, or you're using a deprecated backend). It can be very helpful use the +`symbol` attribute for debugging, as many debugging messages are printed in +Kast format which will be more readable with the `symbol` names you explicitly +declare. In addition, if you are programatically manipulating definitions via +the JSON Kast format, building terms using the user-provided pretty +`symbol, klabel(...)` is easier and less error-prone if the auto-generation process for klabels changes. ### Parametric productions and `bracket` attributes