[An Alpha star]

Alfa

Printing

Alfa supports printing proofs on paper by providing a command to generate LaTeX code from Alfa documents.

There are two ways to print a document:

  1. From an interactive Alfa session: a document can be printed by opening it in Alfa and then selecting the command Print To File... from the File menu. Alfa then suggests a file name ending in .tex in which the LaTeX code will be put.
  2. You can also print directly from the command line, without starting an interactive Alfa session, by starting Alfa with the command line option -print. For example, the command
    alfa evenodd.alfa -print
    will save LaTeX code for the Alfa document evenodd.alfa in the file evenodd.alfa.tex.

The LaTeX code produced by Alfa is designed to be self-contained, but it is not a complete LaTeX document, but rather someting that can be used as part of an article (for example), by including it in the article with the LaTeX command \input.

Example

Assume we want to print the example from the keyboard tutorial, which in the current version of Alfa would look something like this on the screen:

[Def of Bool, Nat, even and odd]

We would then use the Print To File... command in the File menu to obtain a LaTeX file called (for example) evenodd.alfa.tex.

As the next step, we create a main LaTeX file in which we include evenodd.alfa.tex:

\documentclass[a4paper]{article}
\usepackage{isolatin1}
\usepackage{amsmath}
\parindent 0mm
\parskip 5pt

\title{The example with even and odd}
\author{Thomas Hallgren}

\begin{document}
\maketitle

\section{The example with even and odd}

First we define types for truth values and natural numbers.
We then define the two mutually recursive functions $even$ and $odd$.

\input{evenodd.alfa.tex}

\end{document}

Assuming we store this in a file called tst.tex, we can obtain a DVI file with the command

latex tst
and a PostScript file with
dvips tst.dvi -o tst.ps
Take a look at the result:

User influence on how things are printed

The LaTeX code generated is designed to closely resemble what you see on the screen. This means that user defined layout options (argument hiding, infix operator precedence, quantifier notation, etc) are taken into account.

In addition, most of the options in the view menu, and layout options set for individual definitions and expressions, affect what is printed. This is particularly useful in combination with plugin modules that provide alternate views of expressions and definitions. For example, the GF Plugin allows you to produce natural language translation of proofs.

Comments

Any comment in the Alfa document is assumed to contain correct LaTeX code and is thus copied as is to the LaTeX file. This allows you create, e.g., section headings by including them in comments.

LaTeX macros

Alfa uses a small number of LaTeX macros with default definitions that you can override by providing your own definitions:
alfaimport
This macro defines how import definitions are printed. The defualt is to print them as import filename.
alfadeclcomment
This macro defines how comments between definitions are printed. The default is to print them as the are.
alfaexpcomment
This macro defines how comments in expressions are printed. The default is to print them as the are.
As an example, to print comments between definitions in italic, you could include the following definition in your main latex file (the LaTeX file generated by Alfa can be left unchanged):
\newcommand{\alfadeclcomment}[1]{\it #1}

Limitations

LaTeX printing was added to Alfa fairly recently (September 2000), and still has some limitations.

Hopefully, this can be improved in a future version of Alfa.


8 Jan 2003 05:06 Thomas Hallgren
Involuntary disclaimer