[CZT-Users] Re: Help with getting started

[Petra M. <pe...@cs...>]

Hi Stephen,

nice to see that we've got a user that dares to ask questions on this
mailing list.  :-)

Stephen Torri wrote:
> [...] Well I got a few errors that I don't understand:
> 
> storri@base ~/src/czt_0_4_bin/bin $ ./zedtypecheck ~/Documents/StephenTorri/comp7730/project/project.tex
> Jan 27, 2006 12:33:42 AM class net.sourceforge.czt.parser.z.Latex2Unicode
> SEVERE: Unknown latex command \tfun

In short, you are using a latex command that is not defined in the Z
Standard.

Here is a bit more explanation:  There are several Z dialects and
different Z latex commands for those dialects; CZT is an implementation
of the Z Standard and currently only supports the latex commands defined
there.  You can download the Standard for free from the ISO/IEC web-page.

I guess "\tfun" is a total function and is written "\fun" in Standard Z.

> SEVERE: Unknown latex command \times

Use "\cross" instead.

> SEVERE: Unknown latex command \rightarrow

Do you mean "\implies"?

> "/home/storri/Documents/StephenTorri/comp7730/project/project.tex" line 20 column 1: Syntax error at symbol RELATION

You probably want to use "\relation".

> "/home/storri/Documents/StephenTorri/comp7730/project/project.tex" line 30 column 1: Syntax error at symbol PARENTS

You probably want to use "\parents".

> "/home/storri/Documents/StephenTorri/comp7730/project/project.tex" line 97 column 13: Expression expected; found predicate

I have no idea; I would need to have a look at the source latex file to
understand.

Hope that helps,
Petra