History of Changes
Records of changes, starting on 960220.
Changes in 2000-2004
- Experimental: Aarne Ranta's Grammatical
Framework has been plugged in, allowing you view and, to a
limited extent, edit English and Swedish translations of
definitions and expressions. New commands that appear in the
GF: Show in English,
GF: Change English translation of ...,
GF: Give in English, and analogously for Swedish.
- Added the option Auto Abstract to the
Options menu. Initial setting can be changed with the
- Added the option Only refinements from context to the
Options menu. Initial setting can be changed with the
- Experimental: Added the command Print To File... to the
File menu. It saves text much as
Save, but it uses plugin supplied print functions
when selected in the View menu and locally in
declarations and expressions. The intended usage is
to save natural language text produced with the GF plugin.
- The GF plugin is still in a rather experimental state, but it now
supports French in addition to Swedish and English. There is also work
in progress on generating LaTeX code.
- Added Fraction to the layout options available in the
- Made various small updates to the user's guide and related documents
on the web.
- Added Proof style rule to the layout options
available in the Layout Editor. This allows you
to produce proofs that looks nice in natural deduction style at
the same time as you can influence how natural language text is
generating by using different proof rule functions.
- The menu command Print To File... now generates LaTeX
output. The LaTeX result looks nice, but easily becomes too wide to fit
on the page...
- The suggested filename for LaTex output is now the name of the file to
being edited with
.tex added as a suffix.
- The new command line option
causes Alfa to print files in batch mode. As an example, the command line
will produce the files
alfa nat.alfa bool.alfa -print
- Added the command . Projections... to the menu window.
It creates a submenu with projections from variables that could be used
to fill in the current meta variable.
Caveats to be fixed:
- An empty submenu might be shown if no projections are possible.
- The menu window doesn't automatically return
to the main menu after a failed attempt to make a projection, but
you can use any action that normally changes the menu, e.g., moving
the cursor, to get the main menu back.
- The web page on
Printing Alfa documents
was improved and moved.
- Constructor names are now printed in boldface.
- A bug caused by packages occurring in the Projections menu was fixed.
- Experimental: added a command Wrap to simplify
bottom-up construction of expressions.
- The arguments in
open expressions/declarations can now be
selected and deleted.
(Expect to add more commands to manipulate them later.)
Note that selecting the name and the whole argument is not the same.
- Changed how variable names are printed, to make them look nicer
and to avoid problems with accented characters.
- Updated the web page on
Printing Alfa documents
with information on how
comments are printed, and what LaTeX macros that can be used to
influence how things printed.
- Changed how definitions, packages in particular, are printed, to
make them more likely to fit on the page. (Before, complete
defintions were printed in LaTeX's math mode, now they are
printed in paragraph mode, allowing line breaks and page breaks
to be inserted.). This makes them look less similar to what you
see on the screen, however.
- Bug fix: the command to insert a new postulate was not added to the menu.
- Added feature: lambda bound variables can be renamed. (If you
select a lambda bound variable, you actually select a typing, where
the type is hidden, if brief notation is turned on.)
- Infix operators applied to too many arguments are still shown as infix
applications, unless hiding is turned off. E.g., the term
o A B C f g x,
o has 3 hidden arguments, is displayed as
(f o g) x rather than
o f g x,
when hiding is on, and
o A B C f g x, rather than
(A o B) C f g x,
when hiding is turned off.
- Added a horizontal scroll bar to the menu window. (Suggested by
- The proof style Top-Down Proof Tree has been improved
and, after being "work in progress" for a long while, now seems to
to be a useful alternative to Natural Deduction
style proofs, which can easily become rather wide.
An example is shown in the
natural deduction tutorial.
- Improved the way assumptions (i.e., lambda abstractions) are
displayed in proofs. Instead of lambdas, they are now shown with
their names and types in square brackets.
- Fixed a bug introduced on 010319 that could cause Alfa
to crash with "No match in _needParen".
- Instead of always jumping to the next meta variables after an editing
operation, the cursor now only jumps if was on a meta variable before
the editing operation.
- Added Auto Goto Next Goal to the Options
menu, which allow you to
completely turn off cursor jumping after editing operations.
The initial setting can be changed with the
- Improved LaTeX printing:
added conversion of most characters in the symbol font (e.g. greek
letters) to the appropriate LaTeX commands. Also fixed a
bug in the printing of
- Added a flag
-uglymembershipsymbol to make Alfa use
::, instead of the usual set membership symbol, in
- Created a version of Alfa with preliminary support for inductive
families, using Makoto's version of Agda. For the time being, it
is separate from the ordinary version of Alfa, and is started
with the command
ialfa and it is available only on
dogbert (our main development machine).
- Just a small change: When brief notation is off, Alfa now
chooses between horizontal and vertical layout when displaying
(dependent) function types and lambda abstractions.
- Bug fix: Alfa failed to avoid importing the same file twice, if
it was imported via several paths, some of which contained
- Instead of always appearing with a
light, constructors are now filtered and marked
like other entries in the menu.
This will probably not make any difference most of the time,
except for constructors in inductive families (in
- For improved color usage consistency, parentheses, brackets and braces
are now displayed in the keyword/delimiter color.
(See command line options.)
- The line width used for drawing large brackets etc is now adjusted
according to the font size.
- Removed parentheses around some mixfix operator applications that
don't need them.
- Updated the section about layout options in the
- Fixed a font size bug: font sizes were internally numbered 0-6, but
externally 1-7. They are now numbered 1-7 everywhere, and the default
size is 4 instead of 3.
- Add support for associative operators. For example, if
is declared associative, both
a+(b+c) will be displayed as
- Experimental feature:
when specifying mixfix operators, you can now use digits in
_ to specify not only where to put an
argument, but also which argument to put there. For
if _ then _ else _
is equivalent to
if 1 then 2 else 3,
and with today's feature, you could also use
2 if 1, 3 otherwise as an alternative
view of the same operator.
- Support for properties (abstract/private etc) and type
Note: the Agda type checker is likely to fail when
adding a type signature...
- Postfix operator now have a precedence setting, like infix/distfix/mixfix
operators (but no associativity).
- Support for the new mixfix functionality (from 010615) and the
new way of displaying assumptions in proofs (from 010319) in the
- More consistent terminology for commands that add and remove
type annotations in expressions.
- Alfa now uses IAgda (with support for
idata) by default.
- Alfa distributions now contain Michael Hedberg's New library.
(Documentation is under preparation.)
- Alfa now saves all View menu
options except the Font Size.
(Before, only the Argument Hiding option was saved.)
- Added the flag
-termcounter to change Agda's
termination counter (the built-in default value is 1000.)
- The Compute command now appears in the menu with a
red light ,
instead of being absent from the menu, if computation fails.
By selecting the (red)
command, you can get the error message
containing the reason why the computation failed (problably that the
termination counter reached the limit).
- Added the option Simple Refine to the
Options menu. Previously, this option could be set
only with the command line flag
-simplerefine. That flag now sets the default for the menu