Abella Web

Example

Virtual project

Project

No file open.

Pick a file in the project panel to start editing.

Goal Starting…

Privacy abella-prover.org

Keyboard shortcuts

Ctrl/Cmd+Enter: Check to cursor
Ctrl+]: Check next command
Ctrl+[: Undo previous command
Ctrl+Shift+]: Continue checking to the end and focus the editor
Ctrl+Shift+[: Reset the prover
Ctrl+.: Focus and scroll to the checked tip
Ctrl+Space: Show command output near the cursor
Ctrl/Cmd+C in the output dialog: Copy all command output
Ctrl/Cmd+B: Show or hide the project panel
↑/↓ in the project panel: Move through files and folders
→/← in the project panel: Expand or collapse folders, or move to the parent
F2 in the project panel: Rename the selected file
Delete in the project panel: Delete the selected file
Shift+F10: Open the actions menu for the selected file or folder
←/→ in the tab strip: Switch between open files
Ctrl+?: Open this help

The play and step controls check the active .thm or .thmod tab. Switching tabs does not reset the prover; checking a different file does.

Warnings and other command output appear next to the checked command. Hover the command to read it, or click its marker for the full text.

On macOS, use Cmd instead of Ctrl for the Ctrl/Cmd shortcuts. The bracket and dot shortcuts use Ctrl on every platform.

Enforce strict stratification

Treat stratification warnings as errors.

Using system-generated names

Allow, warn about, or forbid references to a hypothesis or variable whose name was not supplied by the user.

Preferences are saved in this browser.

Repository

Use owner/repo, add @branch:folder (branch optional) to narrow the load, or paste any GitHub URL.

Allow private repositories (repo scope)

GitHub sign-in grants account-wide scopes. repo covers all repositories you can access; use a fine-grained token below for per-repository access.

Use a personal access token instead

Fine-grained token

Commit message