Commit d1131ebd authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Added support for `by` and `forall`

parent 79a108a8
......@@ -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. `->`).
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment