On 13 Jul 2012, at 00:10, Julian Bradfield wrote:
>> Latest version requires STIXFonts to be installed. Some other proof
>> assistants use it.
>
> However, that's not true. Isabelle does not need to use Unicode; it
> runs happily in an ASCII terminal, because its internal representation
> is tokens, not Unicode characters. The Unicode is syntactic sugar
> that's part of the Emacs interface and the Scala interface.
I did not check the details, only noting that it will install them.
>>>> If your only objective is to achieve a rendering for humans to read, TeX
>>>> is fine, but not if one wants to communicate semantic information on the
>>>> computer level.
>>>
>>> On the contrary, computers are very happy with TeX notation. There are
>>> several useful mathematical online learning sites (such as, for
>>> example, Alcumus) which use TeX syntax to interact with the students.
>>
>> TeX formulas are just for rendering. For example, if you want to have
>> superscript to the left, you have to write ${}^x y$.
>
> If you read any introduction to TeX, it will explain how you use
> macros to provide a structured markup. If you were using that
> notation, then you would define a suitable macro, say
> \def\tetration#1#2{{}^{#2}{#1}}
> and write $\tetration{y}{x}$.
> This does not depend on any fancy Unicodery for its interpretation,
> and also allows you to define semantic content for the computer.
TeX does not parse the formulas. It cannot see the operator precedences in an
expression like a + b*c. It just renders it. The program you mentioned seems to
not use TeX, but is another computer program using TeX-like syntax (it looked
it departed from strict TeX).
Hans
