Lean App Tutorial, Part 8

This page assumes you've read Parts 1, 2, 3, 4, 5, 6, and 7.

Try the web app live now.

The end of Part 7 promised a tutorial on inserting special symbols into the document, which Lean understands.

Symbols

Lean code can contain many Unicode characters that resemble mathematical notation, and thus make documents more attractive. This appliction supports those characters, as shown in the image below.

The blackboard bold N stands for the natural numbers (formerly written nat) and the greek letter lambda stands for "fun" or "assume" in Lean.

You can enter these symbols by typing a backslash, followed by the symbol's name, followed by the spacebar (or alternately followed by another backslash, if you're starting another symbol immediately afterwards). For example, to type the first line of the document shown above, you would proceed as follows.

  1. Click the button to start a term group.
  2. Type check (3:\nat.
  3. Press the spacebar, and \nat will be replaced by the blackboard bold N.
  4. Type ).

Catalog

What symbols are available? Lots! Nearly 2,000, in fact! But most of them are not useful in Lean itself. Here are three ways to get started with keyboard shortcuts:

  1. The most important ones to know are \and, \or, \to, \neg, \forall, \exists, \pi, \sigma, \lambda, \int, and \nat.
  2. Take the Lean tutorial, which covers the keyboard shortcuts that work in Lean. I imported the same data file into this web app that they use in Lean, so all shortcuts that work in Lean work here.
  3. If you really want to know the full list of 1,959 shortcuts, you can inspect the (minified JSON) data file just mentioned.

So what?

Benefits

Your Lean documents will now look much less computer-ish, and much more mathematical and readable.

Missing pieces

This is the last page of the tutorial, but surely you can think of ways that this app could be improved. Feel free to clone the project and start developing with us! Or contact one of the members of the development team through GitHub. You can also open an issue there for bug reports or feature requests.