Alfa

History of Changes for 1998

980206

• Bug fix: editing operations inside equality constraints in data expressions were lost.
• When adding new declarations, you now give a list of left hand sides (excluding types) instead of just a list of names. For example, when you define the functions even and odd, you could create the new declaration by entering even n, odd n.

980306

• Bug fix: the View menu indicated the Proof Style alternative Hide Trivial Let as active when Alfa started, but Alfa behaved as if Natrual Deduction was active.
• When refining a goal with a quantifier, Alfa automatically makes a lambda abstraction to avoid having to display terms containing a dummy variable.

980323

• Bug fix: when building natural deduction style proof trees by clicking with the middle mouse button, the subgoals were not shown in natural deduction style.
• Bug fix: Superfluous parentheses were sometimes drawn around the bodies of lambda expressions.

980327

• Added the commands Zoom In and Zoom Out to the View menu.
• To make it more likely that the expression you are editing is visible, Alfa now tries to keep the cursor vertically in the center of the window.

980420

• You can now close the browser window. It will reopen next time you browse an imported module.
• Bug fix: clicking on the close button in the title bar of auxiliar windows does not cause Alfa to terminate any longer.
• Constructors are now ommitted from the menu in natural deduction style proofs, since they produce odd looking proofs.

980428

• Bug fix: the OK button in the text pop-up window behaves as the return key, i.e., if the current input is in error, a sad smiley is shown. (Before, the window was closed and the last correct input was used.)
• New command line flag: -multiline causes the text pop-up window to use a multi-line text editor. The makes editing big expressions as text feasible. Drawback: you have to press Meta-Return (instead of just Return) to indicate that the input is complete.

981014

• A first version of Alfa that uses the proof engine Agda instead of V3 is now available. This has been made possible by a complete restructuring and simplification of the interface between Alfa and the proof engine done during the summer. This includes a separation of the abstract syntaxes used by the proof engine and Alfa, meaning that more conversion has to be done, but hopefully the extra communication cost will be negligible.

  The new version of Alfa can not load files created with the old version and vice versa. Except for equality constraints in data definitions, which are not supported by Agda, everything should continue to work as before.

981016

• Alfa now displays constraints all the time, not just when a place holder is selected. Applicable constraints solving commands are displayed in the menu window.

981104

• Improved cursor position after filling in a place holder and the expression is redraw starting from the parent node (or higher) in the syntax tree. (This occurs when refining function types and in natural deduction style proofs, for example.)
• Constructing natural deduction style proofs now works rather well even for predicate logic, thanks to Agda's improved constraing solving tactics.

981201

• Alfa now displays the number of place holder (holes) in the selected expression/declaration(s)/module. Both the number of hidden holes, and the total number of holes are displayed.

981207

• Fixed a bug that caused a parsing error when opening files containing hidden expressions.

981208

• Alfa now understands package, data and open declarations. No menu commans for these constructions have been added yet.

981213

• The Refine... command in the Edit menu now accepts expressions (for example projections) instead of just identifiers.
• Added the option Unfold Goal Types to the View menu.

981221

• You can now rename things. The command Rename identifier... appears in the menu window when the binding occurence of a name is selected.
• Definitions are now shown in an equational style, with case analysis shown as several equations with pattern matching, in the usual functional programming style.

  Example:

  Old, plain style	Equational style

981222

• Circular definitions that previously caused the proof engine to loop are now rejected. (This is implemented by limiting the number of allowed unfold operations during type checking, so in princicple some correct definitions may be rejected. A future version of Alfa may provide an option to change the limit.)