Re: Too narrowly defined: DIVISION SIGN & COLON

From: Hans Aberg <>
Date: Fri, 13 Jul 2012 00:34:17 +0200

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).

Received on Thu Jul 12 2012 - 17:36:26 CDT

This archive was generated by hypermail 2.2.0 : Thu Jul 12 2012 - 17:36:27 CDT