dataexpressions were lost.
odd, you could create the new declaration by entering even n, odd n.
Viewmenu indicated the Proof Style alternative
Hide Trivial Letas active when Alfa started, but Alfa behaved as if
Natrual Deductionwas active.
Zoom Outto the
OKbutton 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.)
-multilinecauses 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.
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.
opendeclarations. No menu commans for these constructions have been added yet.
Refine...command in the
Editmenu now accepts expressions (for example projections) instead of just identifiers.
Unfold Goal Typesto the
Rename identifier...appears in the menu window when the binding occurence of a name is selected.
|Old, plain style||Equational style|