Tutorial - editing by using the keyboard only
This examples shows you how you can enter a small program, around 250
characters long, using about 65 key strokes. You do not have to use
the mouse at all.
Background: the mouse considered harmful
Since the introduction of window system and graphical user interfaces,
the mouse is often used as the primary input device. However, the mouse
is not good for entering text and, since programs and proofs contain
text, it will sometimes be necessary to use the keyboard,
even though most editing operations can be performed with the mouse by
pointing and clicking.
Frequent switching between mouse and keyboard is bad for at least two reasons:
- It slows down the editing.
- It easily makes you overstrain the muscles in the hand and the arm.
This can lead to irreversible damages in the long run.
For these reason, Alfa is designed to allow all editing to be done by
using the keyboard only. Below is an example of a small Alfa
session where all editing is done with the keyboard.
The exercise is to define
- a type Bool for booleans,
- a type Nat for natural numbers,
- the functions even and odd from natural
numbers to booleans.
The result will look like this:
Here is what to do:
You will see the main editing window and the
menu window. Move the mouse pointer inside the main editing
window. After this, you will not have to use the mouse.
Note: the exact key strokes to use may differ between
different versions of Alfa. The correct keys are shown in the
menus. Also, if the cursor happens to end up on the wrong place holder,
you can use Space to move it to the right one.
We first define the type Bool. Here are the required key
- M-d (i.e., Meta-d. The meta key is marked with on Sun keyboards,
Alt on many other keyboards.)
- This the keyboard short-cut for the command
Declaration... in the
- Bool Return
- Enter the name of the thing to be defined in the window that pops
up. Note: you do not have to move the pointer to the pop-up window.
After this the place holder denoting the type of
Bool is selected and the commands for the possible
expressions you could fill in are shown in the menu window:
Bool should be a set.
As shown in the menu, the keyboard short-cut for the type
Set is S.
We should now fill in the definition of Bool.
Bool should be a data type, so we select the
data command from the menu.
- In the window that pops up, we enter the names of the
- False, True Return
The definition of Bool is now complete.
In the same way, we define the type Nat
- M-d Nat Return
- d 0, S n
- N a
The definiton of Nat is now complete.
We continue with the mutually recursive definitions of even
- M-d even odd Return
- Since they are mutually recursive, they have to be defined in the
We now enter the type of both functions, starting with the type
- F . N a B
- Here, F . is the short-cut for creating
function types, N a and B are the short-cuts
for Nat and Bool.
- Move to the place holder for the type of odd
- F . N a B
- This defines the type of odd in the same way.
We now enter the definition of odd.
- This creates a lambda abstraction (the Introduction rule for function
- c a Return
- Case analysis on the variable a.
- $ F
- e n
- Here, e is the short-cut for even and
n is the short-cut for the variable n
introduced in the case expression.
The cursor has moved to the place holder for the definition of
even, which we enter in the same way.
- I c Return
- $ T
- o n
The definitions are now complete! All that is left is saving them in a
- M-a evenodd.alfa