From d1131ebd8f765823e6ec4cbec4de10191b0903db Mon Sep 17 00:00:00 2001 From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com> Date: Wed, 10 Nov 2021 18:31:17 +0100 Subject: [PATCH] Added support for `by` and `forall` --- docs/editor.md | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/docs/editor.md b/docs/editor.md index bce31d0d2..d59d4a550 100644 --- a/docs/editor.md +++ b/docs/editor.md @@ -134,14 +134,16 @@ To solve some of these indentation errors you can add the following line to your initialisation file: ``` (setq coq-smie-user-tokens - '(("∗" . "*") - ("-∗" . "->") - ("∗-∗" . "<->") - ("==∗" . "->") - ("⊢" . "->") - ("⊣⊢" . "<->") - ("⋅" . "*") - (":>" . ":="))) + '(("∗" . "*") + ("-∗" . "->") + ("∗-∗" . "<->") + ("==∗" . "->") + ("⊢" . "->") + ("⊣⊢" . "<->") + ("⋅" . "*") + (":>" . ":=") + ("by" . "now") + ("forall" . "now"))) ``` This will let the indentation strategy treat the Iris symbols (e.g. `-∗`) similar to the closely related Coq symbols (e.g. `->`). -- GitLab