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:

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 example

The exercise is to define The result will look like this:

[The goal of the exercise]

The exercise

Here is what to do: start Alfa. 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.

[The menu window and the main editing window]

We first define the type Bool. Here are the required key strokes:

M-d (i.e., Meta-d. The meta key is marked with a diamond on Sun keyboards, Alt on many other keyboards.)
This the keyboard short-cut for the command New Declaration... in the Edit menu.

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.

[Entering the name of the ting to be defined]

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:

[Skeleton for the definition of Bool and the available menu options]

Bool should be a set. As shown in the menu, the keyboard short-cut for the type Set is S.

[After filling in the type of Bool]

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 constructors.

False, True Return
[Entering the names of the constructors for type Bool]

The definition of Bool is now complete.

[The completed definition of Bool]

In the same way, we define the type Nat:
M-d Nat Return
[A skeleton for the definition of Nat has been added]

d 0, S n Return
[Entering the constructors for type Nat]

N a
[Filling in the type of the argument of the successor constructor]

The definiton of Nat is now complete.

We continue with the mutually recursive definitions of even and odd.
M-d even odd Return
Since they are mutually recursive, they have to be defined in the same declaration.

[Adding the two mutually recursive functions even and odd]

We now enter the type of both functions, starting with the type of even.

[Skeletons for even and odd have been added]

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.

[The type of even has been added]

Move to the place holder for the type of odd

[Moving the cursor to the type of odd]

F . N a B
This defines the type of odd in the same way.

[The types of both even and odd have been filled in]

We now enter the definition of odd.

This creates a lambda abstraction (the Introduction rule for function types).

[Creating a lambda abstraction]

c a Return
Case analysis on the variable a.

[Entering an expression for case analysis]

[The case expression has been created]

$ F
odd 0 = False

[odd 0 = False]

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.

[Completing the definition of odd]

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
[Both even and odd are not complete]
The definitions are now complete! All that is left is saving them in a file.
M-a evenodd.alfa Return
[Save as evenodd.alfa]