Alfa

Overview of the menus

Below, we give a brief description of the purpose of all the commands you find in these menus.

The File menu

The Edit menu

The edit menu contains the following editing operations, some of which should be familiar from other editors.

• Undo and Redo. If the effect of a command was not what you expected, you can undo it by using the undo command. You can go back several steps (10 by default, but you can change this with a command line option). If you went back too far, you can go forward again with the Redo command. An unusual feature of Alfa's undo mechanism is that even the file menu commands New... and Open... can be undone.
• Copy, Paste and Delete. These are fairly standard, except that there is no Cut command. Use Copy, followed by Delete instead.
• New Declaration.... This adds a top level declaration to the end of the document. Futher commands shown in the menu window allow you to insert declarations of various kinds, and at arbitrary places.
• Give.... This command allows you to replace a place holder with an expression entered as text. It is thus only applicable when a place holder is selected. The expression can contain place holders.
• Refine.... This commands allows you to replace a place holder with an expression, applied to the appropriate number of arguments determined by the system. This is the most common step in proof development (since it corresponds to applying a proof rule) and there are several, more convenient ways, to invoke this command. (See Top 10 ways to fill in a place holder.)

The View menu

• Redraw. This commands causes Alfa to redraw the selected expression. This should not be necessary, but if some bug makes the document look strange or incomplete, perhaps this will help.
• Zoom in. This restricts the view to the selected part of the document.
• Zoom out. This returns to the normal state where the editing window shows the entire document.
• Unfold Goal Types.
• Argument Hiding.
• Brief Notation. When this is switched on, contexts (parameter lists), function types, lambda abstraction and case expressions are printed in a more compact form. This means that the concrete syntax that you see doesn't correspond exactly to the abstract syntax actually used behind the scenes, so for some editing operations, you might want to turn this off temporarily.
• Hide Trivial Let. When an expression is selected, you can insert it's type as an annotation by using the command Type annotation. The type is inserted in the expression and shown in the info display. This option makes type annotations inserted in this way invisible. (This command has been renamed to Hide Type Annotations.)
• Default layout: Wide and Tall. Some syntactic units can be presented with two different layouts. This sets which is one is used by default. When an expression is selected, commands appear in the menu window to set the layout to be used for that particular expression.
• Default declaration view: declarations (definitions) can be displayed a number of different ways. The default is to Show complete definitions, showing both the type and the body of the definition. You can also choose to Show type signatures only thus hiding the body of the definition. You can even hide the type signature and Show defined names only. Additional declaration views supplied by plugin modules can appear in the menu as well.

  You can also change the view of individual declarations by using similar commands that appear in the menu window when a declaration is selected. The menu window command Show default declaration view removes the individual view setting from a declaration.

• Proof style: Proofs constructed to be be displayed in natural deduction style can also be shown in two other styles. Plain presents the proof as a plain lambda calculus proof term (at least when combined with the Hide Trivial Let option). Top-Down Proof Tree presents a proof with the goal on top and subproofs below.
• Font size: 1 to 7. Alfa can display text in seven sizes. This selects which of these sizes to use for "normal" text. Subscripts and superscripts are displayed in a smaller size, except if you choose size 1 for normal text, since then there is no smaller size. Big operators are displayed in a larger size, except if you use size 7 for normal text, since then there is no larger size.

The Options menu

Input Mode

Menu mode

Menu Language

Auto Solve Constraints

When a place holder is instantiated, constraints may arise on the possible values of other place holders. When this options is switched on, such constraints are solved and the affected place holders are instantiated, in cases where this is safe, i.e., there is really only one possible solution. When this option is off, no constraints are solved automatically. Instead, commands to apply the automatic solution appear in the menu. You can also manually instantiate the affected place holder. This gives you more control, e.g. if you have a definition a = b and a constraint ?1 = b, the automatic constraint solver would instantiate ?1 to b, but you might prefer to instatiate ?1 to a.

Auto Scroll to center cursor

With this option, Alfa tries to keep the cursor in the center of the window. With this option turned off, the part of the document you are working on might end up near the edge of the window, making it difficult to see what you are doing. With this option turned on, things might jump around too much.

The Utils menu

• Evaluate Expressions. This command opens an auxiliary window where you can enter expressions and evaluate them (compute their normal forms).
• Menu Window. The menu window is opened automatically when Alfa is started, but if you close it, you can re-open it with this command.