Re: [mizar] vocabularies

[Grzegorz Bancerek <bancerek@math.uwb.edu.pl>]

Hi,

Happy New Year

Quoting Josef Urban <urban@ktilinux.ms.mff.cuni.cz>:

> The FM translation technology should rather use notation (pattern) 
> for mapping to TeX than the symbol level, because one Mizar symbol 
> can have very different contexts of use, and possibly very different 
> TeX notations (I think we already talked about this one with Grzegorz 
> some time ago).

In FM translation the only almost but not quite unlike stable resource 
is used:
formats (symbol+arity). For example, plus in expressions x+y, x+, +x etc.
may have different presentation in LaTeX. Namely, the first and third 
pluses are
represented just by + but the second by ^+
Of course, there are bigger differences in translation for other symbols.

Patterns uses types of arguments annotated with constructors which change from
version to version of distribution. Maintenance of translation patterns 
based on
such resource may be quite interesting.

Best,
Grzegorz