Re: [mizar] Strong Mizar wish: linking to consider (fwd)

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Andrea,

>It could be true. For the moment I would be already happy to
>reach some agreement on the representation of mathematical
>EXPRESSIONS.

Are you talking about terms here, or do you also mean
formulas when you say expressions?

>MathML-content provides a good starting point, but we must
>definitely go beyond the K-12 fragment.

By the way: does MathML have a concept of "types"?  Both Coq
and Mizar have it, and I wondered about it (different systems
have different kind of types: in Mizar types only can depend
on terms, in HOL they only can depend on types, and in Coq
they can both depend on terms _and_ types... but that's a
detailed kind of difference, any kind of types in MathML is
okay for me already.)

Freek