Alfa

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.

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

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

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

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.

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.

d

In the window that pops up, we enter the names of the constructors.

False, True Return

The definition of Bool is now complete.

In the same way, we define the type Nat:

M-d Nat Return

S

d 0, S n Return

N a

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.

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

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.

Space

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.

I

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

c a Return

Case analysis on the variable a.

$ F

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.

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

M-a evenodd.alfa Return

Done!