-
Notifications
You must be signed in to change notification settings - Fork 145
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
3 changed files
with
3,583 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,26 @@ | ||
# Lean abbreviations | ||
|
||
This package contains all input abbreviations | ||
used by the [Lean theorem prover](https://leanprover.github.io). | ||
They are the same abbreviations used by the editor plugins | ||
for VS Code, neovim, and (with some differences) Emacs. | ||
|
||
For example, you can type `L\exists \all N` to get `L∃∀N`. | ||
|
||
Please note that the behavior of the espanso expansions | ||
is slightly different from how the editor plugins work: | ||
you need to write the abbreviation name in full, | ||
and you need to type a space after every abbreviation. | ||
|
||
If you want to use a leader character other than `\` | ||
(e.g., `,all ` instead of `\all `), | ||
please check out and adapt the | ||
[Python script](https://github.com/gebner/espanso-lean) | ||
that generates this package. | ||
|
||
## Installation | ||
|
||
Install [espanso](https://espanso.org/install/), then run: | ||
``` | ||
espanso install lean | ||
``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
name: "lean" | ||
title: "Lean input abbreviations" | ||
description: Input abbreviations for unicode symbols for the Lean theorem prover | ||
version: 0.1.0 | ||
author: Gabriel Ebner | ||
tags: ["latex"] |
Oops, something went wrong.