Abella
No description provided
Details
Installs
- Total 76
- Win 65
- Mac 5
- Linux 6
| Oct 26 | Oct 25 | Oct 24 | Oct 23 | Oct 22 | Oct 21 | Oct 20 | Oct 19 | Oct 18 | Oct 17 | Oct 16 | Oct 15 | Oct 14 | Oct 13 | Oct 12 | Oct 11 | Oct 10 | Oct 9 | Oct 8 | Oct 7 | Oct 6 | Oct 5 | Oct 4 | Oct 3 | Oct 2 | Oct 1 | Sep 30 | Sep 29 | Sep 28 | Sep 27 | Sep 26 | Sep 25 | Sep 24 | Sep 23 | Sep 22 | Sep 21 | Sep 20 | Sep 19 | Sep 18 | Sep 17 | Sep 16 | Sep 15 | Sep 14 | Sep 13 | Sep 12 | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Windows | 2 | 4 | 0 | 3 | 1 | 0 | 2 | 3 | 2 | 2 | 1 | 0 | 2 | 5 | 1 | 1 | 1 | 2 | 1 | 1 | 4 | 3 | 3 | 2 | 4 | 2 | 0 | 4 | 2 | 0 | 1 | 2 | 3 | 0 | 1 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| Mac | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
| Linux | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 0 | 0 | 0 | 1 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 3 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
Readme
- Source
- raw.githubusercontent.com
Abella for Sublime Text 3
Support for the Abella theorem prover in Sublime Text 3.
The develop of this plugin is mainly based on a Coq plugin for ST.
Installation
The recommended way to install Sublime Abella is to use Package Control.
It is also possible to install it using git. Navigate to the Sublime Text Packages folder, then run:
git clone git@github.com:JimmyZJX/SublimeAbella.git Abella
Usage
You need to open an Abella script file (*.thm) in ST3, and the following default key bindings should work: - Ctrl+Enter: start Abella if necessary, and navigate to cursor. - Ctrl+Down: navigate to the next statement. - Ctrl+Up: undo last statement - Ctrl+Right: navigate to cursor (basically equivalent to Ctrl+Enter) - Ctrl+Left: reload Abella, and go to cursor - Ctrl+Shift+Enter: kill Abella and reset the state - Ctrl+';': show Theorem
And there are also shortcuts that helps writing proofs: - Ctrl+7: (7 stands for “&”, and) insert text “ /\ ” - Ctrl+'\': ('\' stands for “|”, or) insert text “ \/ ” - Ctrl+'.': ('.' stands for “>”, arrow) insert text “ -> ”
Executable
The abella executable should be in PATH by default.
If you want to change the location, edit your user setting abella.exec and point to the currect file. The default value is abella, and you may change it to \path\to\abella.
Highlighting
In order to get nice background highlighting for the proven parts of the file, add the following snippet to your color scheme file.
For tmTheme syntax:
dark themes
<dict>
<key>name</key>
<string>Proven with Abella</string>
<key>scope</key>
<string>meta.abella.proven</string>
<key>settings</key>
<dict>
<key>background</key>
<string>#365A28</string>
<key>foreground</key>
<string>#51873C</string>
</dict>
</dict>
light themes
<dict>
<key>name</key>
<string>Proven with Abella</string>
<key>scope</key>
<string>meta.abella.proven</string>
<key>settings</key>
<dict>
<key>background</key>
<string>#002800</string>
</dict>
</dict>
For sublime-color-scheme syntax:
dark themes
{
"name": "Proven with Abella",
"scope": "meta.abella.proven",
"background": "#365A28",
"foreground": "#51873C"
},
light themes
{
"name": "Proven with Abella",
"scope": "meta.abella.proven",
"background": "#002800",
},