Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Adam
Iris
Commits
9e44cd34
Commit
9e44cd34
authored
Nov 10, 2021
by
Ralf Jung
Browse files
Merge branch 'indentation_config' into 'master'
Indentation config See merge request
iris/iris!752
parents
6823251d
d1131ebd
Changes
1
Hide whitespace changes
Inline
Side-by-side
docs/editor.md
View file @
9e44cd34
...
...
@@ -125,6 +125,29 @@ results in a decent choice for the symbols used in Iris:
(set-fontset-font t nil (font-spec :name "Symbola"))
```
### Automated Indentation
The default indentation configuration of company-coq is not compatible with the Iris syntax.
As a result, automatic indentation will indent lines incorrectly.
To solve some of these indentation errors you can add the following line to your Emacs
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.
`->`
).
## CoqIDE 8.9 and earlier on Linux (ibus-m17n)
On Linux with old versions of CoqIDE you can use the Intelligent
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment